MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  enfixsn Structured version   Visualization version   GIF version

Theorem enfixsn 8613
Description: Given two equipollent sets, a bijection can always be chosen which fixes a single point. (Contributed by Stefan O'Rear, 9-Jul-2015.)
Assertion
Ref Expression
enfixsn ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝑓,𝑋   𝑓,𝑌

Proof of Theorem enfixsn
Dummy variables 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 1135 . . 3 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑋𝑌)
2 bren 8505 . . 3 (𝑋𝑌 ↔ ∃𝑔 𝑔:𝑋1-1-onto𝑌)
31, 2sylib 221 . 2 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑔 𝑔:𝑋1-1-onto𝑌)
4 relen 8501 . . . . . . . 8 Rel ≈
54brrelex2i 5577 . . . . . . 7 (𝑋𝑌𝑌 ∈ V)
653ad2ant3 1132 . . . . . 6 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑌 ∈ V)
76adantr 484 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑌 ∈ V)
8 f1of 6594 . . . . . . 7 (𝑔:𝑋1-1-onto𝑌𝑔:𝑋𝑌)
98adantl 485 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑔:𝑋𝑌)
10 simpl1 1188 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐴𝑋)
119, 10ffvelrnd 6833 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑔𝐴) ∈ 𝑌)
12 simpl2 1189 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐵𝑌)
13 difsnen 8586 . . . . 5 ((𝑌 ∈ V ∧ (𝑔𝐴) ∈ 𝑌𝐵𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
147, 11, 12, 13syl3anc 1368 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15 bren 8505 . . . 4 ((𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
1614, 15sylib 221 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17 fvex 6662 . . . . . . . . . . 11 (𝑔𝐴) ∈ V
1817a1i 11 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ V)
19 simpl2 1189 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵𝑌)
20 f1osng 6634 . . . . . . . . . 10 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
2118, 19, 20syl2anc 587 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
22 simprr 772 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23 disjdif 4382 . . . . . . . . . 10 ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅
2423a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅)
25 disjdif 4382 . . . . . . . . . 10 ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
2625a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27 f1oun 6613 . . . . . . . . 9 ((({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} ∧ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
2821, 22, 24, 26, 27syl22anc 837 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
298ad2antrl 727 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋𝑌)
30 simpl1 1188 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴𝑋)
3129, 30ffvelrnd 6833 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ 𝑌)
32 uncom 4083 . . . . . . . . . . 11 ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)})
33 difsnid 4706 . . . . . . . . . . 11 ((𝑔𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)}) = 𝑌)
3432, 33syl5eq 2848 . . . . . . . . . 10 ((𝑔𝐴) ∈ 𝑌 → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
3531, 34syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
36 uncom 4083 . . . . . . . . . . 11 ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37 difsnid 4706 . . . . . . . . . . 11 (𝐵𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
3836, 37syl5eq 2848 . . . . . . . . . 10 (𝐵𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
3919, 38syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40 f1oeq23 6586 . . . . . . . . 9 ((({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌))
4135, 39, 40syl2anc 587 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌))
4228, 41mpbid 235 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌)
43 simprl 770 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋1-1-onto𝑌)
44 f1oco 6616 . . . . . . 7 ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌𝑔:𝑋1-1-onto𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
4542, 43, 44syl2anc 587 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
46 f1ofn 6595 . . . . . . . . 9 (𝑔:𝑋1-1-onto𝑌𝑔 Fn 𝑋)
4746ad2antrl 727 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48 fvco2 6739 . . . . . . . 8 ((𝑔 Fn 𝑋𝐴𝑋) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
4947, 30, 48syl2anc 587 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
50 f1ofn 6595 . . . . . . . . 9 ({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
5121, 50syl 17 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
52 f1ofn 6595 . . . . . . . . 9 (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5352ad2antll 728 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5417snid 4564 . . . . . . . . 9 (𝑔𝐴) ∈ {(𝑔𝐴)}
5554a1i 11 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ {(𝑔𝐴)})
56 fvun1 6733 . . . . . . . 8 (({⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)} ∧ Fn (𝑌 ∖ {(𝑔𝐴)}) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ (𝑔𝐴) ∈ {(𝑔𝐴)})) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
5751, 53, 24, 55, 56syl112anc 1371 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
58 fvsng 6923 . . . . . . . 8 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
5918, 19, 58syl2anc 587 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
6049, 57, 593eqtrd 2840 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)
61 snex 5300 . . . . . . . . 9 {⟨(𝑔𝐴), 𝐵⟩} ∈ V
62 vex 3447 . . . . . . . . 9 ∈ V
6361, 62unex 7453 . . . . . . . 8 ({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∈ V
64 vex 3447 . . . . . . . 8 𝑔 ∈ V
6563, 64coex 7621 . . . . . . 7 (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) ∈ V
66 f1oeq1 6583 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓:𝑋1-1-onto𝑌 ↔ (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌))
67 fveq1 6648 . . . . . . . . 9 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓𝐴) = ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴))
6867eqeq1d 2803 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓𝐴) = 𝐵 ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵))
6966, 68anbi12d 633 . . . . . . 7 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵) ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)))
7065, 69spcev 3558 . . . . . 6 (((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7145, 60, 70syl2anc 587 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7271expr 460 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7372exlimdv 1934 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7416, 73mpd 15 . 2 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
753, 74exlimddv 1936 1 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2112  Vcvv 3444  cdif 3881  cun 3882  cin 3883  c0 4246  {csn 4528  cop 4534   class class class wbr 5033  ccom 5527   Fn wfn 6323  wf 6324  1-1-ontowf1o 6327  cfv 6328  cen 8493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-1o 8089  df-er 8276  df-en 8497
This theorem is referenced by:  mapfien2  8860
  Copyright terms: Public domain W3C validator