Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wessf1ornlem Structured version   Visualization version   GIF version

Theorem wessf1ornlem 43882
Description: Given a function 𝐹 on a well-ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
wessf1ornlem.f (πœ‘ β†’ 𝐹 Fn 𝐴)
wessf1ornlem.a (πœ‘ β†’ 𝐴 ∈ 𝑉)
wessf1ornlem.r (πœ‘ β†’ 𝑅 We 𝐴)
wessf1ornlem.g 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯))
Assertion
Ref Expression
wessf1ornlem (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(𝐹 β†Ύ π‘₯):π‘₯–1-1-ontoβ†’ran 𝐹)
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐹,𝑦,𝑧   π‘₯,𝑅,𝑦,𝑧
Allowed substitution hints:   πœ‘(π‘₯,𝑦,𝑧)   𝐴(𝑦,𝑧)   𝐺(π‘₯,𝑦,𝑧)   𝑉(π‘₯,𝑦,𝑧)

Proof of Theorem wessf1ornlem
Dummy variables 𝑑 𝑒 𝑣 𝑀 π‘Ž 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wessf1ornlem.a . . . 4 (πœ‘ β†’ 𝐴 ∈ 𝑉)
2 cnvimass 6081 . . . . . . . 8 (◑𝐹 β€œ {𝑒}) βŠ† dom 𝐹
3 wessf1ornlem.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹 Fn 𝐴)
43fndmd 6655 . . . . . . . . 9 (πœ‘ β†’ dom 𝐹 = 𝐴)
54adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ dom 𝐹 = 𝐴)
62, 5sseqtrid 4035 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴)
7 wessf1ornlem.r . . . . . . . . . 10 (πœ‘ β†’ 𝑅 We 𝐴)
87adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑅 We 𝐴)
92, 4sseqtrid 4035 . . . . . . . . . . 11 (πœ‘ β†’ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴)
101, 9ssexd 5325 . . . . . . . . . 10 (πœ‘ β†’ (◑𝐹 β€œ {𝑒}) ∈ V)
1110adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) ∈ V)
12 inisegn0 6098 . . . . . . . . . . 11 (𝑒 ∈ ran 𝐹 ↔ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
1312biimpi 215 . . . . . . . . . 10 (𝑒 ∈ ran 𝐹 β†’ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
1413adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
15 wereu 5673 . . . . . . . . 9 ((𝑅 We 𝐴 ∧ ((◑𝐹 β€œ {𝑒}) ∈ V ∧ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴 ∧ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
168, 11, 6, 14, 15syl13anc 1373 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
17 riotacl 7383 . . . . . . . 8 (βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ (◑𝐹 β€œ {𝑒}))
1816, 17syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ (◑𝐹 β€œ {𝑒}))
196, 18sseldd 3984 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ 𝐴)
2019ralrimiva 3147 . . . . 5 (πœ‘ β†’ βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ 𝐴)
21 wessf1ornlem.g . . . . . . 7 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯))
22 sneq 4639 . . . . . . . . . . 11 (𝑦 = 𝑒 β†’ {𝑦} = {𝑒})
2322imaeq2d 6060 . . . . . . . . . 10 (𝑦 = 𝑒 β†’ (◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑒}))
2423raleqdv 3326 . . . . . . . . . 10 (𝑦 = 𝑒 β†’ (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯))
2523, 24riotaeqbidv 7368 . . . . . . . . 9 (𝑦 = 𝑒 β†’ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯) = (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯))
26 breq1 5152 . . . . . . . . . . . . 13 (𝑧 = 𝑑 β†’ (𝑧𝑅π‘₯ ↔ 𝑑𝑅π‘₯))
2726notbid 318 . . . . . . . . . . . 12 (𝑧 = 𝑑 β†’ (Β¬ 𝑧𝑅π‘₯ ↔ Β¬ 𝑑𝑅π‘₯))
2827cbvralvw 3235 . . . . . . . . . . 11 (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅π‘₯)
29 breq2 5153 . . . . . . . . . . . . 13 (π‘₯ = 𝑣 β†’ (𝑑𝑅π‘₯ ↔ 𝑑𝑅𝑣))
3029notbid 318 . . . . . . . . . . . 12 (π‘₯ = 𝑣 β†’ (Β¬ 𝑑𝑅π‘₯ ↔ Β¬ 𝑑𝑅𝑣))
3130ralbidv 3178 . . . . . . . . . . 11 (π‘₯ = 𝑣 β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3228, 31bitrid 283 . . . . . . . . . 10 (π‘₯ = 𝑣 β†’ (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3332cbvriotavw 7375 . . . . . . . . 9 (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
3425, 33eqtrdi 2789 . . . . . . . 8 (𝑦 = 𝑒 β†’ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3534cbvmptv 5262 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↦ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯)) = (𝑒 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3621, 35eqtri 2761 . . . . . 6 𝐺 = (𝑒 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3736rnmptss 7122 . . . . 5 (βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ 𝐴 β†’ ran 𝐺 βŠ† 𝐴)
3820, 37syl 17 . . . 4 (πœ‘ β†’ ran 𝐺 βŠ† 𝐴)
391, 38sselpwd 5327 . . 3 (πœ‘ β†’ ran 𝐺 ∈ 𝒫 𝐴)
40 dffn3 6731 . . . . . . 7 (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟢ran 𝐹)
413, 40sylib 217 . . . . . 6 (πœ‘ β†’ 𝐹:𝐴⟢ran 𝐹)
4241, 38fssresd 6759 . . . . 5 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺⟢ran 𝐹)
43 fvres 6911 . . . . . . . . . . . . 13 (𝑀 ∈ ran 𝐺 β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = (πΉβ€˜π‘€))
4443eqcomd 2739 . . . . . . . . . . . 12 (𝑀 ∈ ran 𝐺 β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
4544ad2antrr 725 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
46 simpr 486 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘))
47 fvres 6911 . . . . . . . . . . . 12 (𝑑 ∈ ran 𝐺 β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) = (πΉβ€˜π‘‘))
4847ad2antlr 726 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) = (πΉβ€˜π‘‘))
4945, 46, 483eqtrd 2777 . . . . . . . . . 10 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
50493adantl1 1167 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
51 simpl1 1192 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ πœ‘)
52 simpl3 1194 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑑 ∈ ran 𝐺)
53 simpl2 1193 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 ∈ ran 𝐺)
54 id 22 . . . . . . . . . . . . 13 ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
5554eqcomd 2739 . . . . . . . . . . . 12 ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
5655adantl 483 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
57 eleq1w 2817 . . . . . . . . . . . . . . 15 (𝑏 = 𝑀 β†’ (𝑏 ∈ ran 𝐺 ↔ 𝑀 ∈ ran 𝐺))
58573anbi3d 1443 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺)))
59 fveq2 6892 . . . . . . . . . . . . . . 15 (𝑏 = 𝑀 β†’ (πΉβ€˜π‘) = (πΉβ€˜π‘€))
6059eqeq2d 2744 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ ((πΉβ€˜π‘‘) = (πΉβ€˜π‘) ↔ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)))
6158, 60anbi12d 632 . . . . . . . . . . . . 13 (𝑏 = 𝑀 β†’ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) ↔ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))))
62 breq1 5152 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ (𝑏𝑅𝑑 ↔ 𝑀𝑅𝑑))
6362notbid 318 . . . . . . . . . . . . 13 (𝑏 = 𝑀 β†’ (Β¬ 𝑏𝑅𝑑 ↔ Β¬ 𝑀𝑅𝑑))
6461, 63imbi12d 345 . . . . . . . . . . . 12 (𝑏 = 𝑀 β†’ ((((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑) ↔ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)) β†’ Β¬ 𝑀𝑅𝑑)))
65 eleq1w 2817 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑑 β†’ (π‘Ž ∈ ran 𝐺 ↔ 𝑑 ∈ ran 𝐺))
66653anbi2d 1442 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
67 fveqeq2 6901 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ ((πΉβ€˜π‘Ž) = (πΉβ€˜π‘) ↔ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)))
6866, 67anbi12d 632 . . . . . . . . . . . . . 14 (π‘Ž = 𝑑 β†’ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) ↔ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘))))
69 breq2 5153 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ (π‘π‘…π‘Ž ↔ 𝑏𝑅𝑑))
7069notbid 318 . . . . . . . . . . . . . 14 (π‘Ž = 𝑑 β†’ (Β¬ π‘π‘…π‘Ž ↔ Β¬ 𝑏𝑅𝑑))
7168, 70imbi12d 345 . . . . . . . . . . . . 13 (π‘Ž = 𝑑 β†’ ((((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž) ↔ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑)))
72 eleq1w 2817 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 β†’ (𝑑 ∈ ran 𝐺 ↔ 𝑏 ∈ ran 𝐺))
73723anbi3d 1443 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ↔ (πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
74 fveq2 6892 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘))
7574eqeq2d 2744 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ ((πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘) ↔ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)))
7673, 75anbi12d 632 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 β†’ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) ↔ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘))))
77 breq1 5152 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ (π‘‘π‘…π‘Ž ↔ π‘π‘…π‘Ž))
7877notbid 318 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 β†’ (Β¬ π‘‘π‘…π‘Ž ↔ Β¬ π‘π‘…π‘Ž))
7976, 78imbi12d 345 . . . . . . . . . . . . . 14 (𝑑 = 𝑏 β†’ ((((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž) ↔ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž)))
80 eleq1w 2817 . . . . . . . . . . . . . . . . . 18 (𝑀 = π‘Ž β†’ (𝑀 ∈ ran 𝐺 ↔ π‘Ž ∈ ran 𝐺))
81803anbi2d 1442 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ↔ (πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺)))
82 fveqeq2 6901 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) ↔ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)))
8381, 82anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑀 = π‘Ž β†’ (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ↔ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘))))
84 breq2 5153 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ (𝑑𝑅𝑀 ↔ π‘‘π‘…π‘Ž))
8584notbid 318 . . . . . . . . . . . . . . . 16 (𝑀 = π‘Ž β†’ (Β¬ 𝑑𝑅𝑀 ↔ Β¬ π‘‘π‘…π‘Ž))
8683, 85imbi12d 345 . . . . . . . . . . . . . . 15 (𝑀 = π‘Ž β†’ ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑑𝑅𝑀) ↔ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž)))
8736elrnmpt 5956 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ V β†’ (𝑀 ∈ ran 𝐺 ↔ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)))
8887elv 3481 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ran 𝐺 ↔ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
8988biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ran 𝐺 β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
9089adantr 482 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ran 𝐺 ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
91903ad2antl2 1187 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
92 simp3 1139 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
9392eqcomd 2739 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀)
94 simp11 1204 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ πœ‘)
95 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
96 breq2 5153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑀 β†’ (𝑑𝑅𝑣 ↔ 𝑑𝑅𝑀))
9796notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑀 β†’ (Β¬ 𝑑𝑅𝑣 ↔ Β¬ 𝑑𝑅𝑀))
9897ralbidv 3178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = 𝑀 β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀))
9998cbvriotavw 7375 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
10095, 99eqtr2di 2790 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀)
1011003ad2ant3 1136 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀)
10298cbvreuvw 3401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 ↔ βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
10316, 102sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
104 riota1 7387 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
1061053adant3 1133 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
107101, 106mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀))
108107simpld 496 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 ∈ (◑𝐹 β€œ {𝑒}))
10994, 108syld3an1 1411 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 ∈ (◑𝐹 β€œ {𝑒}))
110 simp2 1138 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑒 ∈ ran 𝐹)
11194, 110, 16syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
11298riota2 7391 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ↔ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀))
113109, 111, 112syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ↔ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀))
11493, 113mpbird 257 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
1151143adant1r 1178 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
11638sselda 3983 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑑 ∈ 𝐴)
1171163adant2 1132 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑑 ∈ 𝐴)
118117adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑑 ∈ 𝐴)
1191183ad2ant1 1134 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑑 ∈ 𝐴)
12055ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
1211203adant3 1133 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
122 fniniseg 7062 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 Fn 𝐴 β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)))
12394, 3, 1223syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)))
124109, 123mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒))
125124simprd 497 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘€) = 𝑒)
1261253adant1r 1178 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘€) = 𝑒)
127121, 126eqtrd 2773 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘‘) = 𝑒)
128 fniniseg 7062 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝐴 β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1293, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1301293ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
131130ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1321313adant3 1133 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
133119, 127, 132mpbir2and 712 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑑 ∈ (◑𝐹 β€œ {𝑒}))
134 rspa 3246 . . . . . . . . . . . . . . . . . 18 ((βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ∧ 𝑑 ∈ (◑𝐹 β€œ {𝑒})) β†’ Β¬ 𝑑𝑅𝑀)
135115, 133, 134syl2anc 585 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ Β¬ 𝑑𝑅𝑀)
136135rexlimdv3a 3160 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ Β¬ 𝑑𝑅𝑀))
13791, 136mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑑𝑅𝑀)
13886, 137chvarvv 2003 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž)
13979, 138chvarvv 2003 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž)
14071, 139chvarvv 2003 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑)
14164, 140chvarvv 2003 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)) β†’ Β¬ 𝑀𝑅𝑑)
14251, 52, 53, 56, 141syl31anc 1374 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑀𝑅𝑑)
143 weso 5668 . . . . . . . . . . . . . 14 (𝑅 We 𝐴 β†’ 𝑅 Or 𝐴)
1447, 143syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 Or 𝐴)
145144adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑅 Or 𝐴)
1461453ad2antl1 1186 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑅 Or 𝐴)
14738sselda 3983 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺) β†’ 𝑀 ∈ 𝐴)
1481473adant3 1133 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑀 ∈ 𝐴)
149148adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 ∈ 𝐴)
150 sotrieq2 5619 . . . . . . . . . . 11 ((𝑅 Or 𝐴 ∧ (𝑀 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴)) β†’ (𝑀 = 𝑑 ↔ (Β¬ 𝑀𝑅𝑑 ∧ Β¬ 𝑑𝑅𝑀)))
151146, 149, 118, 150syl12anc 836 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (𝑀 = 𝑑 ↔ (Β¬ 𝑀𝑅𝑑 ∧ Β¬ 𝑑𝑅𝑀)))
152142, 137, 151mpbir2and 712 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 = 𝑑)
15350, 152syldan 592 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ 𝑀 = 𝑑)
154153ex 414 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ (((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
1551543expb 1121 . . . . . 6 ((πœ‘ ∧ (𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺)) β†’ (((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
156155ralrimivva 3201 . . . . 5 (πœ‘ β†’ βˆ€π‘€ ∈ ran πΊβˆ€π‘‘ ∈ ran 𝐺(((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
157 dff13 7254 . . . . 5 ((𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1β†’ran 𝐹 ↔ ((𝐹 β†Ύ ran 𝐺):ran 𝐺⟢ran 𝐹 ∧ βˆ€π‘€ ∈ ran πΊβˆ€π‘‘ ∈ ran 𝐺(((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑)))
15842, 156, 157sylanbrc 584 . . . 4 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1β†’ran 𝐹)
159 riotaex 7369 . . . . . . . . . . 11 (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V
160159rgenw 3066 . . . . . . . . . 10 βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V
16136fnmpt 6691 . . . . . . . . . 10 (βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V β†’ 𝐺 Fn ran 𝐹)
162160, 161mp1i 13 . . . . . . . . 9 (πœ‘ β†’ 𝐺 Fn ran 𝐹)
163 dffn3 6731 . . . . . . . . 9 (𝐺 Fn ran 𝐹 ↔ 𝐺:ran 𝐹⟢ran 𝐺)
164162, 163sylib 217 . . . . . . . 8 (πœ‘ β†’ 𝐺:ran 𝐹⟢ran 𝐺)
165164ffvelcdmda 7087 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) ∈ ran 𝐺)
166165fvresd 6912 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’)) = (πΉβ€˜(πΊβ€˜π‘’)))
167 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑒 ∈ ran 𝐹)
168159a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V)
16921, 34, 167, 168fvmptd3 7022 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
170169, 18eqeltrd 2834 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}))
171 fvex 6905 . . . . . . . . . . . 12 (πΊβ€˜π‘’) ∈ V
172 eleq1 2822 . . . . . . . . . . . . . 14 (𝑀 = (πΊβ€˜π‘’) β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒})))
173 eleq1 2822 . . . . . . . . . . . . . . 15 (𝑀 = (πΊβ€˜π‘’) β†’ (𝑀 ∈ 𝐴 ↔ (πΊβ€˜π‘’) ∈ 𝐴))
174 fveqeq2 6901 . . . . . . . . . . . . . . 15 (𝑀 = (πΊβ€˜π‘’) β†’ ((πΉβ€˜π‘€) = 𝑒 ↔ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))
175173, 174anbi12d 632 . . . . . . . . . . . . . 14 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
176172, 175bibi12d 346 . . . . . . . . . . . . 13 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)) ↔ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))))
177176imbi2d 341 . . . . . . . . . . . 12 (𝑀 = (πΊβ€˜π‘’) β†’ ((πœ‘ β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒))) ↔ (πœ‘ β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))))
1783, 122syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)))
179171, 177, 178vtocl 3550 . . . . . . . . . . 11 (πœ‘ β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
180179adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
181170, 180mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))
182181simprd 497 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)
183166, 182eqtr2d 2774 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’)))
184 fveq2 6892 . . . . . . . 8 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’)))
185184rspceeqv 3634 . . . . . . 7 (((πΊβ€˜π‘’) ∈ ran 𝐺 ∧ 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’))) β†’ βˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
186165, 183, 185syl2anc 585 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
187186ralrimiva 3147 . . . . 5 (πœ‘ β†’ βˆ€π‘’ ∈ ran πΉβˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
188 dffo3 7104 . . . . 5 ((𝐹 β†Ύ ran 𝐺):ran 𝐺–ontoβ†’ran 𝐹 ↔ ((𝐹 β†Ύ ran 𝐺):ran 𝐺⟢ran 𝐹 ∧ βˆ€π‘’ ∈ ran πΉβˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€)))
18942, 187, 188sylanbrc 584 . . . 4 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–ontoβ†’ran 𝐹)
190 df-f1o 6551 . . . 4 ((𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹 ↔ ((𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1β†’ran 𝐹 ∧ (𝐹 β†Ύ ran 𝐺):ran 𝐺–ontoβ†’ran 𝐹))
191158, 189, 190sylanbrc 584 . . 3 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹)
192 reseq2 5977 . . . . 5 (𝑣 = ran 𝐺 β†’ (𝐹 β†Ύ 𝑣) = (𝐹 β†Ύ ran 𝐺))
193 id 22 . . . . 5 (𝑣 = ran 𝐺 β†’ 𝑣 = ran 𝐺)
194 eqidd 2734 . . . . 5 (𝑣 = ran 𝐺 β†’ ran 𝐹 = ran 𝐹)
195192, 193, 194f1oeq123d 6828 . . . 4 (𝑣 = ran 𝐺 β†’ ((𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹 ↔ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹))
196195rspcev 3613 . . 3 ((ran 𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹) β†’ βˆƒπ‘£ ∈ 𝒫 𝐴(𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹)
19739, 191, 196syl2anc 585 . 2 (πœ‘ β†’ βˆƒπ‘£ ∈ 𝒫 𝐴(𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹)
198 reseq2 5977 . . . 4 (𝑣 = π‘₯ β†’ (𝐹 β†Ύ 𝑣) = (𝐹 β†Ύ π‘₯))
199 id 22 . . . 4 (𝑣 = π‘₯ β†’ 𝑣 = π‘₯)
200 eqidd 2734 . . . 4 (𝑣 = π‘₯ β†’ ran 𝐹 = ran 𝐹)
201198, 199, 200f1oeq123d 6828 . . 3 (𝑣 = π‘₯ β†’ ((𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹 ↔ (𝐹 β†Ύ π‘₯):π‘₯–1-1-ontoβ†’ran 𝐹))
202201cbvrexvw 3236 . 2 (βˆƒπ‘£ ∈ 𝒫 𝐴(𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹 ↔ βˆƒπ‘₯ ∈ 𝒫 𝐴(𝐹 β†Ύ π‘₯):π‘₯–1-1-ontoβ†’ran 𝐹)
203197, 202sylib 217 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(𝐹 β†Ύ π‘₯):π‘₯–1-1-ontoβ†’ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  βˆƒ!wreu 3375  Vcvv 3475   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629   class class class wbr 5149   ↦ cmpt 5232   Or wor 5588   We wwe 5631  β—‘ccnv 5676  dom cdm 5677  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680   Fn wfn 6539  βŸΆwf 6540  β€“1-1β†’wf1 6541  β€“ontoβ†’wfo 6542  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  β„©crio 7364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365
This theorem is referenced by:  wessf1orn  43883
  Copyright terms: Public domain W3C validator