Step | Hyp | Ref
| Expression |
1 | | f1osng 6089 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝑋, 𝑌〉}:{𝑋}–1-1-onto→{𝑌}) |
2 | | f1of 6050 |
. . . . . . 7
⊢
({〈𝑋, 𝑌〉}:{𝑋}–1-1-onto→{𝑌} → {〈𝑋, 𝑌〉}:{𝑋}⟶{𝑌}) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝑋, 𝑌〉}:{𝑋}⟶{𝑌}) |
4 | 3 | 3adant3 1074 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {〈𝑋, 𝑌〉}:{𝑋}⟶{𝑌}) |
5 | | suppsnop.f |
. . . . . 6
⊢ 𝐹 = {〈𝑋, 𝑌〉} |
6 | 5 | feq1i 5949 |
. . . . 5
⊢ (𝐹:{𝑋}⟶{𝑌} ↔ {〈𝑋, 𝑌〉}:{𝑋}⟶{𝑌}) |
7 | 4, 6 | sylibr 223 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝐹:{𝑋}⟶{𝑌}) |
8 | | snex 4835 |
. . . . 5
⊢ {𝑋} ∈ V |
9 | 8 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {𝑋} ∈ V) |
10 | | fex 6394 |
. . . 4
⊢ ((𝐹:{𝑋}⟶{𝑌} ∧ {𝑋} ∈ V) → 𝐹 ∈ V) |
11 | 7, 9, 10 | syl2anc 691 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝐹 ∈ V) |
12 | | simp3 1056 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝑍 ∈ 𝑈) |
13 | | suppval 7184 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}}) |
14 | 11, 12, 13 | syl2anc 691 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}}) |
15 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝐹 = {〈𝑋, 𝑌〉}) |
16 | 15 | dmeqd 5248 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → dom 𝐹 = dom {〈𝑋, 𝑌〉}) |
17 | | dmsnopg 5524 |
. . . . . 6
⊢ (𝑌 ∈ 𝑊 → dom {〈𝑋, 𝑌〉} = {𝑋}) |
18 | 17 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → dom {〈𝑋, 𝑌〉} = {𝑋}) |
19 | 16, 18 | eqtrd 2644 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → dom 𝐹 = {𝑋}) |
20 | | rabeq 3166 |
. . . 4
⊢ (dom
𝐹 = {𝑋} → {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}} = {𝑥 ∈ {𝑋} ∣ (𝐹 “ {𝑥}) ≠ {𝑍}}) |
21 | 19, 20 | syl 17 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}} = {𝑥 ∈ {𝑋} ∣ (𝐹 “ {𝑥}) ≠ {𝑍}}) |
22 | | sneq 4135 |
. . . . . 6
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
23 | 22 | imaeq2d 5385 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐹 “ {𝑥}) = (𝐹 “ {𝑋})) |
24 | 23 | neeq1d 2841 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐹 “ {𝑥}) ≠ {𝑍} ↔ (𝐹 “ {𝑋}) ≠ {𝑍})) |
25 | 24 | rabsnif 4202 |
. . 3
⊢ {𝑥 ∈ {𝑋} ∣ (𝐹 “ {𝑥}) ≠ {𝑍}} = if((𝐹 “ {𝑋}) ≠ {𝑍}, {𝑋}, ∅) |
26 | 21, 25 | syl6eq 2660 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}} = if((𝐹 “ {𝑋}) ≠ {𝑍}, {𝑋}, ∅)) |
27 | | fnsng 5852 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝑋, 𝑌〉} Fn {𝑋}) |
28 | 27 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {〈𝑋, 𝑌〉} Fn {𝑋}) |
29 | 5 | eqcomi 2619 |
. . . . . . . . . 10
⊢
{〈𝑋, 𝑌〉} = 𝐹 |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {〈𝑋, 𝑌〉} = 𝐹) |
31 | 30 | fneq1d 5895 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({〈𝑋, 𝑌〉} Fn {𝑋} ↔ 𝐹 Fn {𝑋})) |
32 | 28, 31 | mpbid 221 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝐹 Fn {𝑋}) |
33 | | snidg 4153 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
34 | 33 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝑋 ∈ {𝑋}) |
35 | | fnsnfv 6168 |
. . . . . . . 8
⊢ ((𝐹 Fn {𝑋} ∧ 𝑋 ∈ {𝑋}) → {(𝐹‘𝑋)} = (𝐹 “ {𝑋})) |
36 | 35 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝐹 Fn {𝑋} ∧ 𝑋 ∈ {𝑋}) → (𝐹 “ {𝑋}) = {(𝐹‘𝑋)}) |
37 | 32, 34, 36 | syl2anc 691 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 “ {𝑋}) = {(𝐹‘𝑋)}) |
38 | 37 | neeq1d 2841 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ((𝐹 “ {𝑋}) ≠ {𝑍} ↔ {(𝐹‘𝑋)} ≠ {𝑍})) |
39 | 5 | fveq1i 6104 |
. . . . . . . 8
⊢ (𝐹‘𝑋) = ({〈𝑋, 𝑌〉}‘𝑋) |
40 | | fvsng 6352 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ({〈𝑋, 𝑌〉}‘𝑋) = 𝑌) |
41 | 40 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({〈𝑋, 𝑌〉}‘𝑋) = 𝑌) |
42 | 39, 41 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹‘𝑋) = 𝑌) |
43 | 42 | sneqd 4137 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {(𝐹‘𝑋)} = {𝑌}) |
44 | 43 | neeq1d 2841 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({(𝐹‘𝑋)} ≠ {𝑍} ↔ {𝑌} ≠ {𝑍})) |
45 | | sneqbg 4314 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑊 → ({𝑌} = {𝑍} ↔ 𝑌 = 𝑍)) |
46 | 45 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({𝑌} = {𝑍} ↔ 𝑌 = 𝑍)) |
47 | 46 | necon3abid 2818 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({𝑌} ≠ {𝑍} ↔ ¬ 𝑌 = 𝑍)) |
48 | 38, 44, 47 | 3bitrd 293 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ((𝐹 “ {𝑋}) ≠ {𝑍} ↔ ¬ 𝑌 = 𝑍)) |
49 | 48 | ifbid 4058 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → if((𝐹 “ {𝑋}) ≠ {𝑍}, {𝑋}, ∅) = if(¬ 𝑌 = 𝑍, {𝑋}, ∅)) |
50 | | ifnot 4083 |
. . 3
⊢ if(¬
𝑌 = 𝑍, {𝑋}, ∅) = if(𝑌 = 𝑍, ∅, {𝑋}) |
51 | 49, 50 | syl6eq 2660 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → if((𝐹 “ {𝑋}) ≠ {𝑍}, {𝑋}, ∅) = if(𝑌 = 𝑍, ∅, {𝑋})) |
52 | 14, 26, 51 | 3eqtrd 2648 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = if(𝑌 = 𝑍, ∅, {𝑋})) |