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

Theorem enfixsn 8110
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 1083 . . 3 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑋𝑌)
2 bren 8006 . . 3 (𝑋𝑌 ↔ ∃𝑔 𝑔:𝑋1-1-onto𝑌)
31, 2sylib 208 . 2 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑔 𝑔:𝑋1-1-onto𝑌)
4 relen 8002 . . . . . . . 8 Rel ≈
54brrelex2i 5193 . . . . . . 7 (𝑋𝑌𝑌 ∈ V)
653ad2ant3 1104 . . . . . 6 ((𝐴𝑋𝐵𝑌𝑋𝑌) → 𝑌 ∈ V)
76adantr 480 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑌 ∈ V)
8 f1of 6175 . . . . . . 7 (𝑔:𝑋1-1-onto𝑌𝑔:𝑋𝑌)
98adantl 481 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝑔:𝑋𝑌)
10 simpl1 1084 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐴𝑋)
119, 10ffvelrnd 6400 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑔𝐴) ∈ 𝑌)
12 simpl2 1085 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → 𝐵𝑌)
13 difsnen 8083 . . . . 5 ((𝑌 ∈ V ∧ (𝑔𝐴) ∈ 𝑌𝐵𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
147, 11, 12, 13syl3anc 1366 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}))
15 bren 8006 . . . 4 ((𝑌 ∖ {(𝑔𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
1614, 15sylib 208 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
17 fvex 6239 . . . . . . . . . . 11 (𝑔𝐴) ∈ V
1817a1i 11 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ V)
19 simpl2 1085 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵𝑌)
20 f1osng 6215 . . . . . . . . . 10 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
2118, 19, 20syl2anc 694 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵})
22 simprr 811 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))
23 disjdif 4073 . . . . . . . . . 10 ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅
2423a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅)
25 disjdif 4073 . . . . . . . . . 10 ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅
2625a1i 11 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)
27 f1oun 6194 . . . . . . . . 9 ((({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} ∧ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
2821, 22, 24, 26, 27syl22anc 1367 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})))
298ad2antrl 764 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋𝑌)
30 simpl1 1084 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴𝑋)
3129, 30ffvelrnd 6400 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ 𝑌)
32 uncom 3790 . . . . . . . . . . 11 ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)})
33 difsnid 4373 . . . . . . . . . . 11 ((𝑔𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔𝐴)}) ∪ {(𝑔𝐴)}) = 𝑌)
3432, 33syl5eq 2697 . . . . . . . . . 10 ((𝑔𝐴) ∈ 𝑌 → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
3531, 34syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌)
36 uncom 3790 . . . . . . . . . . 11 ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵})
37 difsnid 4373 . . . . . . . . . . 11 (𝐵𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌)
3836, 37syl5eq 2697 . . . . . . . . . 10 (𝐵𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
3919, 38syl 17 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌)
40 f1oeq23 6168 . . . . . . . . 9 ((({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ):({(𝑔𝐴)} ∪ (𝑌 ∖ {(𝑔𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌))
4135, 39, 40syl2anc 694 . . . . . . . 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 809 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋1-1-onto𝑌)
44 f1oco 6197 . . . . . . 7 ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ):𝑌1-1-onto𝑌𝑔:𝑋1-1-onto𝑌) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
4542, 43, 44syl2anc 694 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌)
46 f1ofn 6176 . . . . . . . . 9 (𝑔:𝑋1-1-onto𝑌𝑔 Fn 𝑋)
4746ad2antrl 764 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋)
48 fvco2 6312 . . . . . . . 8 ((𝑔 Fn 𝑋𝐴𝑋) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
4947, 30, 48syl2anc 694 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)))
50 f1ofn 6176 . . . . . . . . 9 ({⟨(𝑔𝐴), 𝐵⟩}:{(𝑔𝐴)}–1-1-onto→{𝐵} → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
5121, 50syl 17 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)})
52 f1ofn 6176 . . . . . . . . 9 (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5352ad2antll 765 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → Fn (𝑌 ∖ {(𝑔𝐴)}))
5417snid 4241 . . . . . . . . 9 (𝑔𝐴) ∈ {(𝑔𝐴)}
5554a1i 11 . . . . . . . 8 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔𝐴) ∈ {(𝑔𝐴)})
56 fvun1 6308 . . . . . . . 8 (({⟨(𝑔𝐴), 𝐵⟩} Fn {(𝑔𝐴)} ∧ Fn (𝑌 ∖ {(𝑔𝐴)}) ∧ (({(𝑔𝐴)} ∩ (𝑌 ∖ {(𝑔𝐴)})) = ∅ ∧ (𝑔𝐴) ∈ {(𝑔𝐴)})) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
5751, 53, 24, 55, 56syl112anc 1370 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({⟨(𝑔𝐴), 𝐵⟩} ∪ )‘(𝑔𝐴)) = ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)))
58 fvsng 6488 . . . . . . . 8 (((𝑔𝐴) ∈ V ∧ 𝐵𝑌) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
5918, 19, 58syl2anc 694 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({⟨(𝑔𝐴), 𝐵⟩}‘(𝑔𝐴)) = 𝐵)
6049, 57, 593eqtrd 2689 . . . . . 6 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)
61 snex 4938 . . . . . . . . 9 {⟨(𝑔𝐴), 𝐵⟩} ∈ V
62 vex 3234 . . . . . . . . 9 ∈ V
6361, 62unex 6998 . . . . . . . 8 ({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∈ V
64 vex 3234 . . . . . . . 8 𝑔 ∈ V
6563, 64coex 7160 . . . . . . 7 (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) ∈ V
66 f1oeq1 6165 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓:𝑋1-1-onto𝑌 ↔ (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌))
67 fveq1 6228 . . . . . . . . 9 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → (𝑓𝐴) = ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴))
6867eqeq1d 2653 . . . . . . . 8 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓𝐴) = 𝐵 ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵))
6966, 68anbi12d 747 . . . . . . 7 (𝑓 = (({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔) → ((𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵) ↔ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵)))
7065, 69spcev 3331 . . . . . 6 (((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔):𝑋1-1-onto𝑌 ∧ ((({⟨(𝑔𝐴), 𝐵⟩} ∪ ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7145, 60, 70syl2anc 694 . . . . 5 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ (𝑔:𝑋1-1-onto𝑌:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
7271expr 642 . . . 4 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (:(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7372exlimdv 1901 . . 3 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → (∃ :(𝑌 ∖ {(𝑔𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵)))
7416, 73mpd 15 . 2 (((𝐴𝑋𝐵𝑌𝑋𝑌) ∧ 𝑔:𝑋1-1-onto𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
753, 74exlimddv 1903 1 ((𝐴𝑋𝐵𝑌𝑋𝑌) → ∃𝑓(𝑓:𝑋1-1-onto𝑌 ∧ (𝑓𝐴) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231  cdif 3604  cun 3605  cin 3606  c0 3948  {csn 4210  cop 4216   class class class wbr 4685  ccom 5147   Fn wfn 5921  wf 5922  1-1-ontowf1o 5925  cfv 5926  cen 7994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-1o 7605  df-er 7787  df-en 7998
This theorem is referenced by:  mapfien2  8355
  Copyright terms: Public domain W3C validator