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

Theorem enfixsn 8014
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 1061 . . 3 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑋𝑌)
2 bren 7909 . . 3 (𝑋𝑌 ↔ ∃𝑔 𝑔:𝑋1-1-onto𝑌)
31, 2sylib 208 . 2 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑔 𝑔:𝑋1-1-onto𝑌)
4 relen 7905 . . . . . . . 8 Rel ≈
54brrelex2i 5124 . . . . . . 7 (𝑋𝑌𝑌 ∈ V)
653ad2ant3 1082 . . . . . 6 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑌 ∈ V)
76adantr 481 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑌 ∈ V)
8 f1of 6096 . . . . . . 7 (𝑔:𝑋1-1-onto𝑌𝑔:𝑋𝑌)
98adantl 482 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑔:𝑋𝑌)
10 simpl1 1062 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐴𝑋)
119, 10ffvelrnd 6317 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑔𝐴) ∈ 𝑌)
12 simpl2 1063 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐵𝑌)
13 difsnen 7987 . . . . 5 ((𝑌 ∈ V ∧ (𝑔𝐴) ∈ 𝑌𝐵𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
147, 11, 12, 13syl3anc 1323 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15 bren 7909 . . . 4 ((𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
1614, 15sylib 208 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17 fvex 6160 . . . . . . . . . . 11 (𝑔𝐴) ∈ V
1817a1i 11 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ V)
19 simpl2 1063 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵𝑌)
20 f1osng 6136 . . . . . . . . . 10 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
2118, 19, 20syl2anc 692 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
22 simprr 795 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23 disjdif 4017 . . . . . . . . . 10 ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅
2423a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅)
25 disjdif 4017 . . . . . . . . . 10 ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
2625a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27 f1oun 6115 . . . . . . . . 9 ((({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} ∧ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
2821, 22, 24, 26, 27syl22anc 1324 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
298ad2antrl 763 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋𝑌)
30 simpl1 1062 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴𝑋)
3129, 30ffvelrnd 6317 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ 𝑌)
32 uncom 3740 . . . . . . . . . . 11 ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)})
33 difsnid 4315 . . . . . . . . . . 11 ((𝑔𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)}) = 𝑌)
3432, 33syl5eq 2672 . . . . . . . . . 10 ((𝑔𝐴) ∈ 𝑌 → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
3531, 34syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
36 uncom 3740 . . . . . . . . . . 11 ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37 difsnid 4315 . . . . . . . . . . 11 (𝐵𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
3836, 37syl5eq 2672 . . . . . . . . . 10 (𝐵𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
3919, 38syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40 f1oeq23 6089 . . . . . . . . 9 ((({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌))
4135, 39, 40syl2anc 692 . . . . . . . 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 793 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋1-1-onto𝑌)
44 f1oco 6118 . . . . . . 7 ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌𝑔:𝑋1-1-onto𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
4542, 43, 44syl2anc 692 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
46 f1ofn 6097 . . . . . . . . 9 (𝑔:𝑋1-1-onto𝑌𝑔 Fn 𝑋)
4746ad2antrl 763 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48 fvco2 6231 . . . . . . . 8 ((𝑔 Fn 𝑋𝐴𝑋) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
4947, 30, 48syl2anc 692 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
50 f1ofn 6097 . . . . . . . . 9 ({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
5121, 50syl 17 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
52 f1ofn 6097 . . . . . . . . 9 (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5352ad2antll 764 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5417snid 4184 . . . . . . . . 9 (𝑔𝐴) ∈ {(𝑔𝐴)}
5554a1i 11 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ {(𝑔𝐴)})
56 fvun1 6227 . . . . . . . 8 (({⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)} ∧ Fn (𝑌 ∖ {(𝑔𝐴)}) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ (𝑔𝐴) ∈ {(𝑔𝐴)})) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
5751, 53, 24, 55, 56syl112anc 1327 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
58 fvsng 6402 . . . . . . . 8 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
5918, 19, 58syl2anc 692 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
6049, 57, 593eqtrd 2664 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)
61 snex 4874 . . . . . . . . 9 {⟨(𝑔𝐴), 𝐵⟩} ∈ V
62 vex 3194 . . . . . . . . 9 ∈ V
6361, 62unex 6910 . . . . . . . 8 ({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∈ V
64 vex 3194 . . . . . . . 8 𝑔 ∈ V
6563, 64coex 7068 . . . . . . 7 (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) ∈ V
66 f1oeq1 6086 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓:𝑋1-1-onto𝑌 ↔ (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌))
67 fveq1 6149 . . . . . . . . 9 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓𝐴) = ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴))
6867eqeq1d 2628 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓𝐴) = 𝐵 ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵))
6966, 68anbi12d 746 . . . . . . 7 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵) ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)))
7065, 69spcev 3291 . . . . . 6 (((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7145, 60, 70syl2anc 692 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7271expr 642 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7372exlimdv 1863 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7416, 73mpd 15 . 2 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
753, 74exlimddv 1865 1 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1992  Vcvv 3191  cdif 3557  cun 3558  cin 3559  c0 3896  {csn 4153  cop 4159   class class class wbr 4618  ccom 5083   Fn wfn 5845  wf 5846  1-1-ontowf1o 5849  cfv 5850  cen 7897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-1o 7506  df-er 7688  df-en 7901
This theorem is referenced by:  mapfien2  8259
  Copyright terms: Public domain W3C validator