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

Theorem enfixsn 8222
 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 1130 . . 3 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑋𝑌)
2 bren 8118 . . 3 (𝑋𝑌 ↔ ∃𝑔 𝑔:𝑋1-1-onto𝑌)
31, 2sylib 208 . 2 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑔 𝑔:𝑋1-1-onto𝑌)
4 relen 8114 . . . . . . . 8 Rel ≈
54brrelex2i 5304 . . . . . . 7 (𝑋𝑌𝑌 ∈ V)
653ad2ant3 1127 . . . . . 6 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑌 ∈ V)
76adantr 472 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑌 ∈ V)
8 f1of 6286 . . . . . . 7 (𝑔:𝑋1-1-onto𝑌𝑔:𝑋𝑌)
98adantl 473 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑔:𝑋𝑌)
10 simpl1 1204 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐴𝑋)
119, 10ffvelrnd 6511 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑔𝐴) ∈ 𝑌)
12 simpl2 1206 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐵𝑌)
13 difsnen 8195 . . . . 5 ((𝑌 ∈ V ∧ (𝑔𝐴) ∈ 𝑌𝐵𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
147, 11, 12, 13syl3anc 1463 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15 bren 8118 . . . 4 ((𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
1614, 15sylib 208 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17 fvex 6350 . . . . . . . . . . 11 (𝑔𝐴) ∈ V
1817a1i 11 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ V)
19 simpl2 1206 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵𝑌)
20 f1osng 6326 . . . . . . . . . 10 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
2118, 19, 20syl2anc 696 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
22 simprr 813 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23 disjdif 4172 . . . . . . . . . 10 ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅
2423a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅)
25 disjdif 4172 . . . . . . . . . 10 ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
2625a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27 f1oun 6305 . . . . . . . . 9 ((({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} ∧ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
2821, 22, 24, 26, 27syl22anc 1464 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
298ad2antrl 766 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋𝑌)
30 simpl1 1204 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴𝑋)
3129, 30ffvelrnd 6511 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ 𝑌)
32 uncom 3888 . . . . . . . . . . 11 ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)})
33 difsnid 4474 . . . . . . . . . . 11 ((𝑔𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)}) = 𝑌)
3432, 33syl5eq 2794 . . . . . . . . . 10 ((𝑔𝐴) ∈ 𝑌 → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
3531, 34syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
36 uncom 3888 . . . . . . . . . . 11 ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37 difsnid 4474 . . . . . . . . . . 11 (𝐵𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
3836, 37syl5eq 2794 . . . . . . . . . 10 (𝐵𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
3919, 38syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40 f1oeq23 6279 . . . . . . . . 9 ((({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌))
4135, 39, 40syl2anc 696 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌))
4228, 41mpbid 222 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌)
43 simprl 811 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋1-1-onto𝑌)
44 f1oco 6308 . . . . . . 7 ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌𝑔:𝑋1-1-onto𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
4542, 43, 44syl2anc 696 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
46 f1ofn 6287 . . . . . . . . 9 (𝑔:𝑋1-1-onto𝑌𝑔 Fn 𝑋)
4746ad2antrl 766 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48 fvco2 6423 . . . . . . . 8 ((𝑔 Fn 𝑋𝐴𝑋) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
4947, 30, 48syl2anc 696 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
50 f1ofn 6287 . . . . . . . . 9 ({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
5121, 50syl 17 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
52 f1ofn 6287 . . . . . . . . 9 (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5352ad2antll 767 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5417snid 4341 . . . . . . . . 9 (𝑔𝐴) ∈ {(𝑔𝐴)}
5554a1i 11 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ {(𝑔𝐴)})
56 fvun1 6419 . . . . . . . 8 (({⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)} ∧ Fn (𝑌 ∖ {(𝑔𝐴)}) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ (𝑔𝐴) ∈ {(𝑔𝐴)})) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
5751, 53, 24, 55, 56syl112anc 1467 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
58 fvsng 6599 . . . . . . . 8 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
5918, 19, 58syl2anc 696 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
6049, 57, 593eqtrd 2786 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)
61 snex 5045 . . . . . . . . 9 {⟨(𝑔𝐴), 𝐵⟩} ∈ V
62 vex 3331 . . . . . . . . 9 ∈ V
6361, 62unex 7109 . . . . . . . 8 ({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∈ V
64 vex 3331 . . . . . . . 8 𝑔 ∈ V
6563, 64coex 7271 . . . . . . 7 (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) ∈ V
66 f1oeq1 6276 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓:𝑋1-1-onto𝑌 ↔ (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌))
67 fveq1 6339 . . . . . . . . 9 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓𝐴) = ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴))
6867eqeq1d 2750 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓𝐴) = 𝐵 ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵))
6966, 68anbi12d 749 . . . . . . 7 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵) ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)))
7065, 69spcev 3428 . . . . . 6 (((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7145, 60, 70syl2anc 696 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7271expr 644 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7372exlimdv 1998 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7416, 73mpd 15 . 2 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
753, 74exlimddv 2000 1 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1620  ∃wex 1841   ∈ wcel 2127  Vcvv 3328   ∖ cdif 3700   ∪ cun 3701   ∩ cin 3702  ∅c0 4046  {csn 4309  ⟨cop 4315   class class class wbr 4792   ∘ ccom 5258   Fn wfn 6032  ⟶wf 6033  –1-1-onto→wf1o 6036  ‘cfv 6037   ≈ cen 8106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-1o 7717  df-er 7899  df-en 8110 This theorem is referenced by:  mapfien2  8467
 Copyright terms: Public domain W3C validator