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

Theorem enfixsn 8946
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 1137 . . 3 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑋𝑌)
2 bren 8814 . . 3 (𝑋𝑌 ↔ ∃𝑔 𝑔:𝑋1-1-onto𝑌)
31, 2sylib 217 . 2 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑔 𝑔:𝑋1-1-onto𝑌)
4 relen 8809 . . . . . . . 8 Rel ≈
54brrelex2i 5675 . . . . . . 7 (𝑋𝑌𝑌 ∈ V)
653ad2ant3 1134 . . . . . 6 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑌 ∈ V)
76adantr 481 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑌 ∈ V)
8 f1of 6767 . . . . . . 7 (𝑔:𝑋1-1-onto𝑌𝑔:𝑋𝑌)
98adantl 482 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑔:𝑋𝑌)
10 simpl1 1190 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐴𝑋)
119, 10ffvelcdmd 7018 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑔𝐴) ∈ 𝑌)
12 simpl2 1191 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐵𝑌)
13 difsnen 8918 . . . . 5 ((𝑌 ∈ V ∧ (𝑔𝐴) ∈ 𝑌𝐵𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
147, 11, 12, 13syl3anc 1370 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15 bren 8814 . . . 4 ((𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
1614, 15sylib 217 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17 fvex 6838 . . . . . . . . . . 11 (𝑔𝐴) ∈ V
1817a1i 11 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ V)
19 simpl2 1191 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵𝑌)
20 f1osng 6808 . . . . . . . . . 10 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
2118, 19, 20syl2anc 584 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
22 simprr 770 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23 disjdif 4418 . . . . . . . . . 10 ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅
2423a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅)
25 disjdif 4418 . . . . . . . . . 10 ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
2625a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27 f1oun 6786 . . . . . . . . 9 ((({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} ∧ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
2821, 22, 24, 26, 27syl22anc 836 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
298ad2antrl 725 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋𝑌)
30 simpl1 1190 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴𝑋)
3129, 30ffvelcdmd 7018 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ 𝑌)
32 uncom 4100 . . . . . . . . . . 11 ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)})
33 difsnid 4757 . . . . . . . . . . 11 ((𝑔𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)}) = 𝑌)
3432, 33eqtrid 2788 . . . . . . . . . 10 ((𝑔𝐴) ∈ 𝑌 → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
3531, 34syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
36 uncom 4100 . . . . . . . . . . 11 ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37 difsnid 4757 . . . . . . . . . . 11 (𝐵𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
3836, 37eqtrid 2788 . . . . . . . . . 10 (𝐵𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
3919, 38syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40 f1oeq23 6758 . . . . . . . . 9 ((({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌))
4135, 39, 40syl2anc 584 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌))
4228, 41mpbid 231 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌)
43 simprl 768 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋1-1-onto𝑌)
44 f1oco 6790 . . . . . . 7 ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌𝑔:𝑋1-1-onto𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
4542, 43, 44syl2anc 584 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
46 f1ofn 6768 . . . . . . . . 9 (𝑔:𝑋1-1-onto𝑌𝑔 Fn 𝑋)
4746ad2antrl 725 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48 fvco2 6921 . . . . . . . 8 ((𝑔 Fn 𝑋𝐴𝑋) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
4947, 30, 48syl2anc 584 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
50 f1ofn 6768 . . . . . . . . 9 ({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
5121, 50syl 17 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
52 f1ofn 6768 . . . . . . . . 9 (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5352ad2antll 726 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5417snid 4609 . . . . . . . . 9 (𝑔𝐴) ∈ {(𝑔𝐴)}
5554a1i 11 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ {(𝑔𝐴)})
56 fvun1 6915 . . . . . . . 8 (({⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)} ∧ Fn (𝑌 ∖ {(𝑔𝐴)}) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ (𝑔𝐴) ∈ {(𝑔𝐴)})) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
5751, 53, 24, 55, 56syl112anc 1373 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
58 fvsng 7108 . . . . . . . 8 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
5918, 19, 58syl2anc 584 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
6049, 57, 593eqtrd 2780 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)
61 snex 5376 . . . . . . . . 9 {⟨(𝑔𝐴), 𝐵⟩} ∈ V
62 vex 3445 . . . . . . . . 9 ∈ V
6361, 62unex 7658 . . . . . . . 8 ({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∈ V
64 vex 3445 . . . . . . . 8 𝑔 ∈ V
6563, 64coex 7845 . . . . . . 7 (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) ∈ V
66 f1oeq1 6755 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓:𝑋1-1-onto𝑌 ↔ (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌))
67 fveq1 6824 . . . . . . . . 9 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓𝐴) = ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴))
6867eqeq1d 2738 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓𝐴) = 𝐵 ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵))
6966, 68anbi12d 631 . . . . . . 7 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵) ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)))
7065, 69spcev 3554 . . . . . 6 (((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7145, 60, 70syl2anc 584 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7271expr 457 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7372exlimdv 1935 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7416, 73mpd 15 . 2 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
753, 74exlimddv 1937 1 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  Vcvv 3441  cdif 3895  cun 3896  cin 3897  c0 4269  {csn 4573  cop 4579   class class class wbr 5092  ccom 5624   Fn wfn 6474  wf 6475  1-1-ontowf1o 6478  cfv 6479  cen 8801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-en 8805
This theorem is referenced by:  mapfien2  9266
  Copyright terms: Public domain W3C validator