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 44184
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 480 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ dom 𝐹 = 𝐴)
62, 5sseqtrid 4035 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴)
7 wessf1ornlem.r . . . . . . . . . 10 (πœ‘ β†’ 𝑅 We 𝐴)
87adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑅 We 𝐴)
92, 4sseqtrid 4035 . . . . . . . . . . 11 (πœ‘ β†’ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴)
101, 9ssexd 5325 . . . . . . . . . 10 (πœ‘ β†’ (◑𝐹 β€œ {𝑒}) ∈ V)
1110adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) ∈ V)
12 inisegn0 6098 . . . . . . . . . . 11 (𝑒 ∈ ran 𝐹 ↔ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
1312biimpi 215 . . . . . . . . . 10 (𝑒 ∈ ran 𝐹 β†’ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
1413adantl 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
15 wereu 5673 . . . . . . . . 9 ((𝑅 We 𝐴 ∧ ((◑𝐹 β€œ {𝑒}) ∈ V ∧ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴 ∧ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
168, 11, 6, 14, 15syl13anc 1371 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
17 riotacl 7386 . . . . . . . 8 (βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ (◑𝐹 β€œ {𝑒}))
1816, 17syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ (◑𝐹 β€œ {𝑒}))
196, 18sseldd 3984 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ 𝐴)
2019ralrimiva 3145 . . . . 5 (πœ‘ β†’ βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ 𝐴)
21 wessf1ornlem.g . . . . . . 7 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯))
22 sneq 4639 . . . . . . . . . . 11 (𝑦 = 𝑒 β†’ {𝑦} = {𝑒})
2322imaeq2d 6060 . . . . . . . . . 10 (𝑦 = 𝑒 β†’ (◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑒}))
2423raleqdv 3324 . . . . . . . . . 10 (𝑦 = 𝑒 β†’ (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯))
2523, 24riotaeqbidv 7371 . . . . . . . . 9 (𝑦 = 𝑒 β†’ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯) = (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯))
26 breq1 5152 . . . . . . . . . . . . 13 (𝑧 = 𝑑 β†’ (𝑧𝑅π‘₯ ↔ 𝑑𝑅π‘₯))
2726notbid 317 . . . . . . . . . . . 12 (𝑧 = 𝑑 β†’ (Β¬ 𝑧𝑅π‘₯ ↔ Β¬ 𝑑𝑅π‘₯))
2827cbvralvw 3233 . . . . . . . . . . 11 (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅π‘₯)
29 breq2 5153 . . . . . . . . . . . . 13 (π‘₯ = 𝑣 β†’ (𝑑𝑅π‘₯ ↔ 𝑑𝑅𝑣))
3029notbid 317 . . . . . . . . . . . 12 (π‘₯ = 𝑣 β†’ (Β¬ 𝑑𝑅π‘₯ ↔ Β¬ 𝑑𝑅𝑣))
3130ralbidv 3176 . . . . . . . . . . 11 (π‘₯ = 𝑣 β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3228, 31bitrid 282 . . . . . . . . . 10 (π‘₯ = 𝑣 β†’ (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3332cbvriotavw 7378 . . . . . . . . 9 (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
3425, 33eqtrdi 2787 . . . . . . . 8 (𝑦 = 𝑒 β†’ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3534cbvmptv 5262 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↦ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯)) = (𝑒 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3621, 35eqtri 2759 . . . . . 6 𝐺 = (𝑒 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3736rnmptss 7125 . . . . 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 2737 . . . . . . . . . . . 12 (𝑀 ∈ ran 𝐺 β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
4544ad2antrr 723 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
46 simpr 484 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘))
47 fvres 6911 . . . . . . . . . . . 12 (𝑑 ∈ ran 𝐺 β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) = (πΉβ€˜π‘‘))
4847ad2antlr 724 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) = (πΉβ€˜π‘‘))
4945, 46, 483eqtrd 2775 . . . . . . . . . 10 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
50493adantl1 1165 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
51 simpl1 1190 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ πœ‘)
52 simpl3 1192 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑑 ∈ ran 𝐺)
53 simpl2 1191 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 ∈ ran 𝐺)
54 id 22 . . . . . . . . . . . . 13 ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
5554eqcomd 2737 . . . . . . . . . . . 12 ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
5655adantl 481 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
57 eleq1w 2815 . . . . . . . . . . . . . . 15 (𝑏 = 𝑀 β†’ (𝑏 ∈ ran 𝐺 ↔ 𝑀 ∈ ran 𝐺))
58573anbi3d 1441 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺)))
59 fveq2 6892 . . . . . . . . . . . . . . 15 (𝑏 = 𝑀 β†’ (πΉβ€˜π‘) = (πΉβ€˜π‘€))
6059eqeq2d 2742 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ ((πΉβ€˜π‘‘) = (πΉβ€˜π‘) ↔ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)))
6158, 60anbi12d 630 . . . . . . . . . . . . 13 (𝑏 = 𝑀 β†’ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) ↔ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))))
62 breq1 5152 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ (𝑏𝑅𝑑 ↔ 𝑀𝑅𝑑))
6362notbid 317 . . . . . . . . . . . . 13 (𝑏 = 𝑀 β†’ (Β¬ 𝑏𝑅𝑑 ↔ Β¬ 𝑀𝑅𝑑))
6461, 63imbi12d 343 . . . . . . . . . . . 12 (𝑏 = 𝑀 β†’ ((((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑) ↔ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)) β†’ Β¬ 𝑀𝑅𝑑)))
65 eleq1w 2815 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑑 β†’ (π‘Ž ∈ ran 𝐺 ↔ 𝑑 ∈ ran 𝐺))
66653anbi2d 1440 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
67 fveqeq2 6901 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ ((πΉβ€˜π‘Ž) = (πΉβ€˜π‘) ↔ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)))
6866, 67anbi12d 630 . . . . . . . . . . . . . 14 (π‘Ž = 𝑑 β†’ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) ↔ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘))))
69 breq2 5153 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ (π‘π‘…π‘Ž ↔ 𝑏𝑅𝑑))
7069notbid 317 . . . . . . . . . . . . . 14 (π‘Ž = 𝑑 β†’ (Β¬ π‘π‘…π‘Ž ↔ Β¬ 𝑏𝑅𝑑))
7168, 70imbi12d 343 . . . . . . . . . . . . 13 (π‘Ž = 𝑑 β†’ ((((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž) ↔ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑)))
72 eleq1w 2815 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 β†’ (𝑑 ∈ ran 𝐺 ↔ 𝑏 ∈ ran 𝐺))
73723anbi3d 1441 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ↔ (πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
74 fveq2 6892 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘))
7574eqeq2d 2742 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ ((πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘) ↔ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)))
7673, 75anbi12d 630 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 β†’ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) ↔ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘))))
77 breq1 5152 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ (π‘‘π‘…π‘Ž ↔ π‘π‘…π‘Ž))
7877notbid 317 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 β†’ (Β¬ π‘‘π‘…π‘Ž ↔ Β¬ π‘π‘…π‘Ž))
7976, 78imbi12d 343 . . . . . . . . . . . . . 14 (𝑑 = 𝑏 β†’ ((((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž) ↔ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž)))
80 eleq1w 2815 . . . . . . . . . . . . . . . . . 18 (𝑀 = π‘Ž β†’ (𝑀 ∈ ran 𝐺 ↔ π‘Ž ∈ ran 𝐺))
81803anbi2d 1440 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ↔ (πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺)))
82 fveqeq2 6901 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) ↔ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)))
8381, 82anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑀 = π‘Ž β†’ (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ↔ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘))))
84 breq2 5153 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ (𝑑𝑅𝑀 ↔ π‘‘π‘…π‘Ž))
8584notbid 317 . . . . . . . . . . . . . . . 16 (𝑀 = π‘Ž β†’ (Β¬ 𝑑𝑅𝑀 ↔ Β¬ π‘‘π‘…π‘Ž))
8683, 85imbi12d 343 . . . . . . . . . . . . . . 15 (𝑀 = π‘Ž β†’ ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑑𝑅𝑀) ↔ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž)))
8736elrnmpt 5956 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ V β†’ (𝑀 ∈ ran 𝐺 ↔ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)))
8887elv 3479 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ran 𝐺 ↔ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
8988biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ran 𝐺 β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
9089adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ran 𝐺 ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
91903ad2antl2 1185 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
92 simp3 1137 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
9392eqcomd 2737 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀)
94 simp11 1202 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ πœ‘)
95 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
96 breq2 5153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑀 β†’ (𝑑𝑅𝑣 ↔ 𝑑𝑅𝑀))
9796notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑀 β†’ (Β¬ 𝑑𝑅𝑣 ↔ Β¬ 𝑑𝑅𝑀))
9897ralbidv 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = 𝑀 β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀))
9998cbvriotavw 7378 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
10095, 99eqtr2di 2788 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀)
1011003ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀)
10298cbvreuvw 3399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 ↔ βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
10316, 102sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
104 riota1 7390 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
1061053adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
107101, 106mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀))
108107simpld 494 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 ∈ (◑𝐹 β€œ {𝑒}))
10994, 108syld3an1 1409 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 ∈ (◑𝐹 β€œ {𝑒}))
110 simp2 1136 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑒 ∈ ran 𝐹)
11194, 110, 16syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
11298riota2 7394 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ↔ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀))
113109, 111, 112syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ↔ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀))
11493, 113mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
1151143adant1r 1176 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
11638sselda 3983 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑑 ∈ 𝐴)
1171163adant2 1130 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑑 ∈ 𝐴)
118117adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑑 ∈ 𝐴)
1191183ad2ant1 1132 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑑 ∈ 𝐴)
12055ad2antlr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
1211203adant3 1131 . . . . . . . . . . . . . . . . . . . 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 495 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘€) = 𝑒)
1261253adant1r 1176 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘€) = 𝑒)
127121, 126eqtrd 2771 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘‘) = 𝑒)
128 fniniseg 7062 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝐴 β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1293, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1301293ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
131130ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1321313adant3 1131 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
133119, 127, 132mpbir2and 710 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑑 ∈ (◑𝐹 β€œ {𝑒}))
134 rspa 3244 . . . . . . . . . . . . . . . . . 18 ((βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ∧ 𝑑 ∈ (◑𝐹 β€œ {𝑒})) β†’ Β¬ 𝑑𝑅𝑀)
135115, 133, 134syl2anc 583 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ Β¬ 𝑑𝑅𝑀)
136135rexlimdv3a 3158 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ Β¬ 𝑑𝑅𝑀))
13791, 136mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑑𝑅𝑀)
13886, 137chvarvv 2001 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž)
13979, 138chvarvv 2001 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž)
14071, 139chvarvv 2001 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑)
14164, 140chvarvv 2001 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)) β†’ Β¬ 𝑀𝑅𝑑)
14251, 52, 53, 56, 141syl31anc 1372 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑀𝑅𝑑)
143 weso 5668 . . . . . . . . . . . . . 14 (𝑅 We 𝐴 β†’ 𝑅 Or 𝐴)
1447, 143syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 Or 𝐴)
145144adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑅 Or 𝐴)
1461453ad2antl1 1184 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑅 Or 𝐴)
14738sselda 3983 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺) β†’ 𝑀 ∈ 𝐴)
1481473adant3 1131 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑀 ∈ 𝐴)
149148adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 ∈ 𝐴)
150 sotrieq2 5619 . . . . . . . . . . 11 ((𝑅 Or 𝐴 ∧ (𝑀 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴)) β†’ (𝑀 = 𝑑 ↔ (Β¬ 𝑀𝑅𝑑 ∧ Β¬ 𝑑𝑅𝑀)))
151146, 149, 118, 150syl12anc 834 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (𝑀 = 𝑑 ↔ (Β¬ 𝑀𝑅𝑑 ∧ Β¬ 𝑑𝑅𝑀)))
152142, 137, 151mpbir2and 710 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 = 𝑑)
15350, 152syldan 590 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ 𝑀 = 𝑑)
154153ex 412 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ (((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
1551543expb 1119 . . . . . 6 ((πœ‘ ∧ (𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺)) β†’ (((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
156155ralrimivva 3199 . . . . 5 (πœ‘ β†’ βˆ€π‘€ ∈ ran πΊβˆ€π‘‘ ∈ ran 𝐺(((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
157 dff13 7257 . . . . 5 ((𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1β†’ran 𝐹 ↔ ((𝐹 β†Ύ ran 𝐺):ran 𝐺⟢ran 𝐹 ∧ βˆ€π‘€ ∈ ran πΊβˆ€π‘‘ ∈ ran 𝐺(((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑)))
15842, 156, 157sylanbrc 582 . . . 4 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1β†’ran 𝐹)
159 riotaex 7372 . . . . . . . . . . 11 (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V
160159rgenw 3064 . . . . . . . . . 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 484 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑒 ∈ ran 𝐹)
168159a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V)
16921, 34, 167, 168fvmptd3 7022 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
170169, 18eqeltrd 2832 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}))
171 fvex 6905 . . . . . . . . . . . 12 (πΊβ€˜π‘’) ∈ V
172 eleq1 2820 . . . . . . . . . . . . . 14 (𝑀 = (πΊβ€˜π‘’) β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒})))
173 eleq1 2820 . . . . . . . . . . . . . . 15 (𝑀 = (πΊβ€˜π‘’) β†’ (𝑀 ∈ 𝐴 ↔ (πΊβ€˜π‘’) ∈ 𝐴))
174 fveqeq2 6901 . . . . . . . . . . . . . . 15 (𝑀 = (πΊβ€˜π‘’) β†’ ((πΉβ€˜π‘€) = 𝑒 ↔ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))
175173, 174anbi12d 630 . . . . . . . . . . . . . 14 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
176172, 175bibi12d 344 . . . . . . . . . . . . 13 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)) ↔ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))))
177176imbi2d 339 . . . . . . . . . . . 12 (𝑀 = (πΊβ€˜π‘’) β†’ ((πœ‘ β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒))) ↔ (πœ‘ β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))))
1783, 122syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)))
179171, 177, 178vtocl 3541 . . . . . . . . . . 11 (πœ‘ β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
180179adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
181170, 180mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))
182181simprd 495 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)
183166, 182eqtr2d 2772 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’)))
184 fveq2 6892 . . . . . . . 8 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’)))
185184rspceeqv 3634 . . . . . . 7 (((πΊβ€˜π‘’) ∈ ran 𝐺 ∧ 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’))) β†’ βˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
186165, 183, 185syl2anc 583 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
187186ralrimiva 3145 . . . . 5 (πœ‘ β†’ βˆ€π‘’ ∈ ran πΉβˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
188 dffo3 7104 . . . . 5 ((𝐹 β†Ύ ran 𝐺):ran 𝐺–ontoβ†’ran 𝐹 ↔ ((𝐹 β†Ύ ran 𝐺):ran 𝐺⟢ran 𝐹 ∧ βˆ€π‘’ ∈ ran πΉβˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€)))
18942, 187, 188sylanbrc 582 . . . 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 582 . . 3 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹)
192 reseq2 5977 . . . . 5 (𝑣 = ran 𝐺 β†’ (𝐹 β†Ύ 𝑣) = (𝐹 β†Ύ ran 𝐺))
193 id 22 . . . . 5 (𝑣 = ran 𝐺 β†’ 𝑣 = ran 𝐺)
194 eqidd 2732 . . . . 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 583 . 2 (πœ‘ β†’ βˆƒπ‘£ ∈ 𝒫 𝐴(𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹)
198 reseq2 5977 . . . 4 (𝑣 = π‘₯ β†’ (𝐹 β†Ύ 𝑣) = (𝐹 β†Ύ π‘₯))
199 id 22 . . . 4 (𝑣 = π‘₯ β†’ 𝑣 = π‘₯)
200 eqidd 2732 . . . 4 (𝑣 = π‘₯ β†’ ran 𝐹 = ran 𝐹)
201198, 199, 200f1oeq123d 6828 . . 3 (𝑣 = π‘₯ β†’ ((𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹 ↔ (𝐹 β†Ύ π‘₯):π‘₯–1-1-ontoβ†’ran 𝐹))
202201cbvrexvw 3234 . 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 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  βˆ€wral 3060  βˆƒwrex 3069  βˆƒ!wreu 3373  Vcvv 3473   βŠ† 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 7367
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 2702  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  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 7368
This theorem is referenced by:  wessf1orn  44185
  Copyright terms: Public domain W3C validator