Step | Hyp | Ref
| Expression |
1 | | f1osng 6177 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝑋, 𝑌〉}:{𝑋}–1-1-onto→{𝑌}) |
2 | | f1of 6137 |
. . . . . . 7
⊢
({〈𝑋, 𝑌〉}:{𝑋}–1-1-onto→{𝑌} → {〈𝑋, 𝑌〉}:{𝑋}⟶{𝑌}) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝑋, 𝑌〉}:{𝑋}⟶{𝑌}) |
4 | 3 | 3adant3 1081 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {〈𝑋, 𝑌〉}:{𝑋}⟶{𝑌}) |
5 | | suppsnop.f |
. . . . . 6
⊢ 𝐹 = {〈𝑋, 𝑌〉} |
6 | 5 | feq1i 6036 |
. . . . 5
⊢ (𝐹:{𝑋}⟶{𝑌} ↔ {〈𝑋, 𝑌〉}:{𝑋}⟶{𝑌}) |
7 | 4, 6 | sylibr 224 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝐹:{𝑋}⟶{𝑌}) |
8 | | snex 4908 |
. . . . 5
⊢ {𝑋} ∈ V |
9 | 8 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {𝑋} ∈ V) |
10 | | fex 6490 |
. . . 4
⊢ ((𝐹:{𝑋}⟶{𝑌} ∧ {𝑋} ∈ V) → 𝐹 ∈ V) |
11 | 7, 9, 10 | syl2anc 693 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝐹 ∈ V) |
12 | | simp3 1063 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝑍 ∈ 𝑈) |
13 | | suppval 7297 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}}) |
14 | 11, 12, 13 | syl2anc 693 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}}) |
15 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝐹 = {〈𝑋, 𝑌〉}) |
16 | 15 | dmeqd 5326 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → dom 𝐹 = dom {〈𝑋, 𝑌〉}) |
17 | | dmsnopg 5606 |
. . . . . 6
⊢ (𝑌 ∈ 𝑊 → dom {〈𝑋, 𝑌〉} = {𝑋}) |
18 | 17 | 3ad2ant2 1083 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → dom {〈𝑋, 𝑌〉} = {𝑋}) |
19 | 16, 18 | eqtrd 2656 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → dom 𝐹 = {𝑋}) |
20 | | rabeq 3192 |
. . . 4
⊢ (dom
𝐹 = {𝑋} → {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}} = {𝑥 ∈ {𝑋} ∣ (𝐹 “ {𝑥}) ≠ {𝑍}}) |
21 | 19, 20 | syl 17 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}} = {𝑥 ∈ {𝑋} ∣ (𝐹 “ {𝑥}) ≠ {𝑍}}) |
22 | | sneq 4187 |
. . . . . 6
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
23 | 22 | imaeq2d 5466 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐹 “ {𝑥}) = (𝐹 “ {𝑋})) |
24 | 23 | neeq1d 2853 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐹 “ {𝑥}) ≠ {𝑍} ↔ (𝐹 “ {𝑋}) ≠ {𝑍})) |
25 | 24 | rabsnif 4258 |
. . 3
⊢ {𝑥 ∈ {𝑋} ∣ (𝐹 “ {𝑥}) ≠ {𝑍}} = if((𝐹 “ {𝑋}) ≠ {𝑍}, {𝑋}, ∅) |
26 | 21, 25 | syl6eq 2672 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {𝑥 ∈ dom 𝐹 ∣ (𝐹 “ {𝑥}) ≠ {𝑍}} = if((𝐹 “ {𝑋}) ≠ {𝑍}, {𝑋}, ∅)) |
27 | | fnsng 5938 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝑋, 𝑌〉} Fn {𝑋}) |
28 | 27 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {〈𝑋, 𝑌〉} Fn {𝑋}) |
29 | 5 | eqcomi 2631 |
. . . . . . . . . 10
⊢
{〈𝑋, 𝑌〉} = 𝐹 |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {〈𝑋, 𝑌〉} = 𝐹) |
31 | 30 | fneq1d 5981 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({〈𝑋, 𝑌〉} Fn {𝑋} ↔ 𝐹 Fn {𝑋})) |
32 | 28, 31 | mpbid 222 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝐹 Fn {𝑋}) |
33 | | snidg 4206 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
34 | 33 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → 𝑋 ∈ {𝑋}) |
35 | | fnsnfv 6258 |
. . . . . . . 8
⊢ ((𝐹 Fn {𝑋} ∧ 𝑋 ∈ {𝑋}) → {(𝐹‘𝑋)} = (𝐹 “ {𝑋})) |
36 | 35 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝐹 Fn {𝑋} ∧ 𝑋 ∈ {𝑋}) → (𝐹 “ {𝑋}) = {(𝐹‘𝑋)}) |
37 | 32, 34, 36 | syl2anc 693 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 “ {𝑋}) = {(𝐹‘𝑋)}) |
38 | 37 | neeq1d 2853 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ((𝐹 “ {𝑋}) ≠ {𝑍} ↔ {(𝐹‘𝑋)} ≠ {𝑍})) |
39 | 5 | fveq1i 6192 |
. . . . . . . 8
⊢ (𝐹‘𝑋) = ({〈𝑋, 𝑌〉}‘𝑋) |
40 | | fvsng 6447 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ({〈𝑋, 𝑌〉}‘𝑋) = 𝑌) |
41 | 40 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({〈𝑋, 𝑌〉}‘𝑋) = 𝑌) |
42 | 39, 41 | syl5eq 2668 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹‘𝑋) = 𝑌) |
43 | 42 | sneqd 4189 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {(𝐹‘𝑋)} = {𝑌}) |
44 | 43 | neeq1d 2853 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({(𝐹‘𝑋)} ≠ {𝑍} ↔ {𝑌} ≠ {𝑍})) |
45 | | sneqbg 4374 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑊 → ({𝑌} = {𝑍} ↔ 𝑌 = 𝑍)) |
46 | 45 | 3ad2ant2 1083 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({𝑌} = {𝑍} ↔ 𝑌 = 𝑍)) |
47 | 46 | necon3abid 2830 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ({𝑌} ≠ {𝑍} ↔ ¬ 𝑌 = 𝑍)) |
48 | 38, 44, 47 | 3bitrd 294 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → ((𝐹 “ {𝑋}) ≠ {𝑍} ↔ ¬ 𝑌 = 𝑍)) |
49 | 48 | ifbid 4108 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → if((𝐹 “ {𝑋}) ≠ {𝑍}, {𝑋}, ∅) = if(¬ 𝑌 = 𝑍, {𝑋}, ∅)) |
50 | | ifnot 4133 |
. . 3
⊢ if(¬
𝑌 = 𝑍, {𝑋}, ∅) = if(𝑌 = 𝑍, ∅, {𝑋}) |
51 | 49, 50 | syl6eq 2672 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → if((𝐹 “ {𝑋}) ≠ {𝑍}, {𝑋}, ∅) = if(𝑌 = 𝑍, ∅, {𝑋})) |
52 | 14, 26, 51 | 3eqtrd 2660 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = if(𝑌 = 𝑍, ∅, {𝑋})) |