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 43969
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 6080 . . . . . . . 8 (◑𝐹 β€œ {𝑒}) βŠ† dom 𝐹
3 wessf1ornlem.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹 Fn 𝐴)
43fndmd 6654 . . . . . . . . 9 (πœ‘ β†’ dom 𝐹 = 𝐴)
54adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ dom 𝐹 = 𝐴)
62, 5sseqtrid 4034 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴)
7 wessf1ornlem.r . . . . . . . . . 10 (πœ‘ β†’ 𝑅 We 𝐴)
87adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑅 We 𝐴)
92, 4sseqtrid 4034 . . . . . . . . . . 11 (πœ‘ β†’ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴)
101, 9ssexd 5324 . . . . . . . . . 10 (πœ‘ β†’ (◑𝐹 β€œ {𝑒}) ∈ V)
1110adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) ∈ V)
12 inisegn0 6097 . . . . . . . . . . 11 (𝑒 ∈ ran 𝐹 ↔ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
1312biimpi 215 . . . . . . . . . 10 (𝑒 ∈ ran 𝐹 β†’ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
1413adantl 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)
15 wereu 5672 . . . . . . . . 9 ((𝑅 We 𝐴 ∧ ((◑𝐹 β€œ {𝑒}) ∈ V ∧ (◑𝐹 β€œ {𝑒}) βŠ† 𝐴 ∧ (◑𝐹 β€œ {𝑒}) β‰  βˆ…)) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
168, 11, 6, 14, 15syl13anc 1372 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
17 riotacl 7385 . . . . . . . 8 (βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ (◑𝐹 β€œ {𝑒}))
1816, 17syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ (◑𝐹 β€œ {𝑒}))
196, 18sseldd 3983 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ 𝐴)
2019ralrimiva 3146 . . . . 5 (πœ‘ β†’ βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ 𝐴)
21 wessf1ornlem.g . . . . . . 7 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯))
22 sneq 4638 . . . . . . . . . . 11 (𝑦 = 𝑒 β†’ {𝑦} = {𝑒})
2322imaeq2d 6059 . . . . . . . . . 10 (𝑦 = 𝑒 β†’ (◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑒}))
2423raleqdv 3325 . . . . . . . . . 10 (𝑦 = 𝑒 β†’ (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯))
2523, 24riotaeqbidv 7370 . . . . . . . . 9 (𝑦 = 𝑒 β†’ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯) = (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯))
26 breq1 5151 . . . . . . . . . . . . 13 (𝑧 = 𝑑 β†’ (𝑧𝑅π‘₯ ↔ 𝑑𝑅π‘₯))
2726notbid 317 . . . . . . . . . . . 12 (𝑧 = 𝑑 β†’ (Β¬ 𝑧𝑅π‘₯ ↔ Β¬ 𝑑𝑅π‘₯))
2827cbvralvw 3234 . . . . . . . . . . 11 (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅π‘₯)
29 breq2 5152 . . . . . . . . . . . . 13 (π‘₯ = 𝑣 β†’ (𝑑𝑅π‘₯ ↔ 𝑑𝑅𝑣))
3029notbid 317 . . . . . . . . . . . 12 (π‘₯ = 𝑣 β†’ (Β¬ 𝑑𝑅π‘₯ ↔ Β¬ 𝑑𝑅𝑣))
3130ralbidv 3177 . . . . . . . . . . 11 (π‘₯ = 𝑣 β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3228, 31bitrid 282 . . . . . . . . . 10 (π‘₯ = 𝑣 β†’ (βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯ ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3332cbvriotavw 7377 . . . . . . . . 9 (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑧𝑅π‘₯) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
3425, 33eqtrdi 2788 . . . . . . . 8 (𝑦 = 𝑒 β†’ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3534cbvmptv 5261 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↦ (β„©π‘₯ ∈ (◑𝐹 β€œ {𝑦})βˆ€π‘§ ∈ (◑𝐹 β€œ {𝑦}) Β¬ 𝑧𝑅π‘₯)) = (𝑒 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3621, 35eqtri 2760 . . . . . 6 𝐺 = (𝑒 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
3736rnmptss 7124 . . . . 5 (βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ 𝐴 β†’ ran 𝐺 βŠ† 𝐴)
3820, 37syl 17 . . . 4 (πœ‘ β†’ ran 𝐺 βŠ† 𝐴)
391, 38sselpwd 5326 . . 3 (πœ‘ β†’ ran 𝐺 ∈ 𝒫 𝐴)
40 dffn3 6730 . . . . . . 7 (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟢ran 𝐹)
413, 40sylib 217 . . . . . 6 (πœ‘ β†’ 𝐹:𝐴⟢ran 𝐹)
4241, 38fssresd 6758 . . . . 5 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺⟢ran 𝐹)
43 fvres 6910 . . . . . . . . . . . . 13 (𝑀 ∈ ran 𝐺 β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = (πΉβ€˜π‘€))
4443eqcomd 2738 . . . . . . . . . . . 12 (𝑀 ∈ ran 𝐺 β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
4544ad2antrr 724 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
46 simpr 485 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘))
47 fvres 6910 . . . . . . . . . . . 12 (𝑑 ∈ ran 𝐺 β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) = (πΉβ€˜π‘‘))
4847ad2antlr 725 . . . . . . . . . . 11 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) = (πΉβ€˜π‘‘))
4945, 46, 483eqtrd 2776 . . . . . . . . . 10 (((𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
50493adantl1 1166 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
51 simpl1 1191 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ πœ‘)
52 simpl3 1193 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑑 ∈ ran 𝐺)
53 simpl2 1192 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 ∈ ran 𝐺)
54 id 22 . . . . . . . . . . . . 13 ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) β†’ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘))
5554eqcomd 2738 . . . . . . . . . . . 12 ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
5655adantl 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
57 eleq1w 2816 . . . . . . . . . . . . . . 15 (𝑏 = 𝑀 β†’ (𝑏 ∈ ran 𝐺 ↔ 𝑀 ∈ ran 𝐺))
58573anbi3d 1442 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺)))
59 fveq2 6891 . . . . . . . . . . . . . . 15 (𝑏 = 𝑀 β†’ (πΉβ€˜π‘) = (πΉβ€˜π‘€))
6059eqeq2d 2743 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ ((πΉβ€˜π‘‘) = (πΉβ€˜π‘) ↔ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)))
6158, 60anbi12d 631 . . . . . . . . . . . . 13 (𝑏 = 𝑀 β†’ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) ↔ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))))
62 breq1 5151 . . . . . . . . . . . . . 14 (𝑏 = 𝑀 β†’ (𝑏𝑅𝑑 ↔ 𝑀𝑅𝑑))
6362notbid 317 . . . . . . . . . . . . 13 (𝑏 = 𝑀 β†’ (Β¬ 𝑏𝑅𝑑 ↔ Β¬ 𝑀𝑅𝑑))
6461, 63imbi12d 344 . . . . . . . . . . . 12 (𝑏 = 𝑀 β†’ ((((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑) ↔ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)) β†’ Β¬ 𝑀𝑅𝑑)))
65 eleq1w 2816 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑑 β†’ (π‘Ž ∈ ran 𝐺 ↔ 𝑑 ∈ ran 𝐺))
66653anbi2d 1441 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
67 fveqeq2 6900 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ ((πΉβ€˜π‘Ž) = (πΉβ€˜π‘) ↔ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)))
6866, 67anbi12d 631 . . . . . . . . . . . . . 14 (π‘Ž = 𝑑 β†’ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) ↔ ((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘))))
69 breq2 5152 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑑 β†’ (π‘π‘…π‘Ž ↔ 𝑏𝑅𝑑))
7069notbid 317 . . . . . . . . . . . . . 14 (π‘Ž = 𝑑 β†’ (Β¬ π‘π‘…π‘Ž ↔ Β¬ 𝑏𝑅𝑑))
7168, 70imbi12d 344 . . . . . . . . . . . . 13 (π‘Ž = 𝑑 β†’ ((((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž) ↔ (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑)))
72 eleq1w 2816 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 β†’ (𝑑 ∈ ran 𝐺 ↔ 𝑏 ∈ ran 𝐺))
73723anbi3d 1442 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ↔ (πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺)))
74 fveq2 6891 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘))
7574eqeq2d 2743 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ ((πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘) ↔ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)))
7673, 75anbi12d 631 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 β†’ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) ↔ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘))))
77 breq1 5151 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 β†’ (π‘‘π‘…π‘Ž ↔ π‘π‘…π‘Ž))
7877notbid 317 . . . . . . . . . . . . . . 15 (𝑑 = 𝑏 β†’ (Β¬ π‘‘π‘…π‘Ž ↔ Β¬ π‘π‘…π‘Ž))
7976, 78imbi12d 344 . . . . . . . . . . . . . 14 (𝑑 = 𝑏 β†’ ((((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž) ↔ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž)))
80 eleq1w 2816 . . . . . . . . . . . . . . . . . 18 (𝑀 = π‘Ž β†’ (𝑀 ∈ ran 𝐺 ↔ π‘Ž ∈ ran 𝐺))
81803anbi2d 1441 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ↔ (πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺)))
82 fveqeq2 6900 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ ((πΉβ€˜π‘€) = (πΉβ€˜π‘‘) ↔ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)))
8381, 82anbi12d 631 . . . . . . . . . . . . . . . 16 (𝑀 = π‘Ž β†’ (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ↔ ((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘))))
84 breq2 5152 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘Ž β†’ (𝑑𝑅𝑀 ↔ π‘‘π‘…π‘Ž))
8584notbid 317 . . . . . . . . . . . . . . . 16 (𝑀 = π‘Ž β†’ (Β¬ 𝑑𝑅𝑀 ↔ Β¬ π‘‘π‘…π‘Ž))
8683, 85imbi12d 344 . . . . . . . . . . . . . . 15 (𝑀 = π‘Ž β†’ ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑑𝑅𝑀) ↔ (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž)))
8736elrnmpt 5955 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ V β†’ (𝑀 ∈ ran 𝐺 ↔ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)))
8887elv 3480 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ran 𝐺 ↔ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
8988biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ran 𝐺 β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
9089adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ran 𝐺 ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
91903ad2antl2 1186 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
92 simp3 1138 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
9392eqcomd 2738 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀)
94 simp11 1203 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ πœ‘)
95 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
96 breq2 5152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑀 β†’ (𝑑𝑅𝑣 ↔ 𝑑𝑅𝑀))
9796notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑀 β†’ (Β¬ 𝑑𝑅𝑣 ↔ Β¬ 𝑑𝑅𝑀))
9897ralbidv 3177 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = 𝑀 β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 ↔ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀))
9998cbvriotavw 7377 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
10095, 99eqtr2di 2789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀)
1011003ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀)
10298cbvreuvw 3400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣 ↔ βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
10316, 102sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
104 riota1 7389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆƒ!𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
1061053adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) ↔ (℩𝑀 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀) = 𝑀))
107101, 106mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀))
108107simpld 495 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 ∈ (◑𝐹 β€œ {𝑒}))
10994, 108syld3an1 1410 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑀 ∈ (◑𝐹 β€œ {𝑒}))
110 simp2 1137 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑒 ∈ ran 𝐹)
11194, 110, 16syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)
11298riota2 7393 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ∧ βˆƒ!𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ↔ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀))
113109, 111, 112syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ↔ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) = 𝑀))
11493, 113mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
1151143adant1r 1177 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀)
11638sselda 3982 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑑 ∈ 𝐴)
1171163adant2 1131 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑑 ∈ 𝐴)
118117adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑑 ∈ 𝐴)
1191183ad2ant1 1133 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑑 ∈ 𝐴)
12055ad2antlr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
1211203adant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€))
122 fniniseg 7061 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 Fn 𝐴 β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)))
12394, 3, 1223syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)))
124109, 123mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒))
125124simprd 496 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘€) = 𝑒)
1261253adant1r 1177 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘€) = 𝑒)
127121, 126eqtrd 2772 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (πΉβ€˜π‘‘) = 𝑒)
128 fniniseg 7061 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝐴 β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1293, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1301293ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
131130ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
1321313adant3 1132 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ (𝑑 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑑 ∈ 𝐴 ∧ (πΉβ€˜π‘‘) = 𝑒)))
133119, 127, 132mpbir2and 711 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ 𝑑 ∈ (◑𝐹 β€œ {𝑒}))
134 rspa 3245 . . . . . . . . . . . . . . . . . 18 ((βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑀 ∧ 𝑑 ∈ (◑𝐹 β€œ {𝑒})) β†’ Β¬ 𝑑𝑅𝑀)
135115, 133, 134syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) ∧ 𝑒 ∈ ran 𝐹 ∧ 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣)) β†’ Β¬ 𝑑𝑅𝑀)
136135rexlimdv3a 3159 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (βˆƒπ‘’ ∈ ran 𝐹 𝑀 = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) β†’ Β¬ 𝑑𝑅𝑀))
13791, 136mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑑𝑅𝑀)
13886, 137chvarvv 2002 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘‘)) β†’ Β¬ π‘‘π‘…π‘Ž)
13979, 138chvarvv 2002 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ž ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘)) β†’ Β¬ π‘π‘…π‘Ž)
14071, 139chvarvv 2002 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘)) β†’ Β¬ 𝑏𝑅𝑑)
14164, 140chvarvv 2002 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ ran 𝐺 ∧ 𝑀 ∈ ran 𝐺) ∧ (πΉβ€˜π‘‘) = (πΉβ€˜π‘€)) β†’ Β¬ 𝑀𝑅𝑑)
14251, 52, 53, 56, 141syl31anc 1373 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ Β¬ 𝑀𝑅𝑑)
143 weso 5667 . . . . . . . . . . . . . 14 (𝑅 We 𝐴 β†’ 𝑅 Or 𝐴)
1447, 143syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 Or 𝐴)
145144adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑅 Or 𝐴)
1461453ad2antl1 1185 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑅 Or 𝐴)
14738sselda 3982 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺) β†’ 𝑀 ∈ 𝐴)
1481473adant3 1132 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ 𝑀 ∈ 𝐴)
149148adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 ∈ 𝐴)
150 sotrieq2 5618 . . . . . . . . . . 11 ((𝑅 Or 𝐴 ∧ (𝑀 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴)) β†’ (𝑀 = 𝑑 ↔ (Β¬ 𝑀𝑅𝑑 ∧ Β¬ 𝑑𝑅𝑀)))
151146, 149, 118, 150syl12anc 835 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ (𝑀 = 𝑑 ↔ (Β¬ 𝑀𝑅𝑑 ∧ Β¬ 𝑑𝑅𝑀)))
152142, 137, 151mpbir2and 711 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ (πΉβ€˜π‘€) = (πΉβ€˜π‘‘)) β†’ 𝑀 = 𝑑)
15350, 152syldan 591 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘)) β†’ 𝑀 = 𝑑)
154153ex 413 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺) β†’ (((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
1551543expb 1120 . . . . . 6 ((πœ‘ ∧ (𝑀 ∈ ran 𝐺 ∧ 𝑑 ∈ ran 𝐺)) β†’ (((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
156155ralrimivva 3200 . . . . 5 (πœ‘ β†’ βˆ€π‘€ ∈ ran πΊβˆ€π‘‘ ∈ ran 𝐺(((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑))
157 dff13 7256 . . . . 5 ((𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1β†’ran 𝐹 ↔ ((𝐹 β†Ύ ran 𝐺):ran 𝐺⟢ran 𝐹 ∧ βˆ€π‘€ ∈ ran πΊβˆ€π‘‘ ∈ ran 𝐺(((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜π‘‘) β†’ 𝑀 = 𝑑)))
15842, 156, 157sylanbrc 583 . . . 4 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1β†’ran 𝐹)
159 riotaex 7371 . . . . . . . . . . 11 (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V
160159rgenw 3065 . . . . . . . . . 10 βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V
16136fnmpt 6690 . . . . . . . . . 10 (βˆ€π‘’ ∈ ran 𝐹(℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V β†’ 𝐺 Fn ran 𝐹)
162160, 161mp1i 13 . . . . . . . . 9 (πœ‘ β†’ 𝐺 Fn ran 𝐹)
163 dffn3 6730 . . . . . . . . 9 (𝐺 Fn ran 𝐹 ↔ 𝐺:ran 𝐹⟢ran 𝐺)
164162, 163sylib 217 . . . . . . . 8 (πœ‘ β†’ 𝐺:ran 𝐹⟢ran 𝐺)
165164ffvelcdmda 7086 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) ∈ ran 𝐺)
166165fvresd 6911 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’)) = (πΉβ€˜(πΊβ€˜π‘’)))
167 simpr 485 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑒 ∈ ran 𝐹)
168159a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣) ∈ V)
16921, 34, 167, 168fvmptd3 7021 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) = (℩𝑣 ∈ (◑𝐹 β€œ {𝑒})βˆ€π‘‘ ∈ (◑𝐹 β€œ {𝑒}) Β¬ 𝑑𝑅𝑣))
170169, 18eqeltrd 2833 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}))
171 fvex 6904 . . . . . . . . . . . 12 (πΊβ€˜π‘’) ∈ V
172 eleq1 2821 . . . . . . . . . . . . . 14 (𝑀 = (πΊβ€˜π‘’) β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒})))
173 eleq1 2821 . . . . . . . . . . . . . . 15 (𝑀 = (πΊβ€˜π‘’) β†’ (𝑀 ∈ 𝐴 ↔ (πΊβ€˜π‘’) ∈ 𝐴))
174 fveqeq2 6900 . . . . . . . . . . . . . . 15 (𝑀 = (πΊβ€˜π‘’) β†’ ((πΉβ€˜π‘€) = 𝑒 ↔ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))
175173, 174anbi12d 631 . . . . . . . . . . . . . 14 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
176172, 175bibi12d 345 . . . . . . . . . . . . 13 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)) ↔ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))))
177176imbi2d 340 . . . . . . . . . . . 12 (𝑀 = (πΊβ€˜π‘’) β†’ ((πœ‘ β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒))) ↔ (πœ‘ β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))))
1783, 122syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑀 ∈ (◑𝐹 β€œ {𝑒}) ↔ (𝑀 ∈ 𝐴 ∧ (πΉβ€˜π‘€) = 𝑒)))
179171, 177, 178vtocl 3549 . . . . . . . . . . 11 (πœ‘ β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
180179adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((πΊβ€˜π‘’) ∈ (◑𝐹 β€œ {𝑒}) ↔ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)))
181170, 180mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ ((πΊβ€˜π‘’) ∈ 𝐴 ∧ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒))
182181simprd 496 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΉβ€˜(πΊβ€˜π‘’)) = 𝑒)
183166, 182eqtr2d 2773 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’)))
184 fveq2 6891 . . . . . . . 8 (𝑀 = (πΊβ€˜π‘’) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘€) = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’)))
185184rspceeqv 3633 . . . . . . 7 (((πΊβ€˜π‘’) ∈ ran 𝐺 ∧ 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜(πΊβ€˜π‘’))) β†’ βˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
186165, 183, 185syl2anc 584 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
187186ralrimiva 3146 . . . . 5 (πœ‘ β†’ βˆ€π‘’ ∈ ran πΉβˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€))
188 dffo3 7103 . . . . 5 ((𝐹 β†Ύ ran 𝐺):ran 𝐺–ontoβ†’ran 𝐹 ↔ ((𝐹 β†Ύ ran 𝐺):ran 𝐺⟢ran 𝐹 ∧ βˆ€π‘’ ∈ ran πΉβˆƒπ‘€ ∈ ran 𝐺 𝑒 = ((𝐹 β†Ύ ran 𝐺)β€˜π‘€)))
18942, 187, 188sylanbrc 583 . . . 4 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–ontoβ†’ran 𝐹)
190 df-f1o 6550 . . . 4 ((𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹 ↔ ((𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1β†’ran 𝐹 ∧ (𝐹 β†Ύ ran 𝐺):ran 𝐺–ontoβ†’ran 𝐹))
191158, 189, 190sylanbrc 583 . . 3 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹)
192 reseq2 5976 . . . . 5 (𝑣 = ran 𝐺 β†’ (𝐹 β†Ύ 𝑣) = (𝐹 β†Ύ ran 𝐺))
193 id 22 . . . . 5 (𝑣 = ran 𝐺 β†’ 𝑣 = ran 𝐺)
194 eqidd 2733 . . . . 5 (𝑣 = ran 𝐺 β†’ ran 𝐹 = ran 𝐹)
195192, 193, 194f1oeq123d 6827 . . . 4 (𝑣 = ran 𝐺 β†’ ((𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹 ↔ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹))
196195rspcev 3612 . . 3 ((ran 𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹) β†’ βˆƒπ‘£ ∈ 𝒫 𝐴(𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹)
19739, 191, 196syl2anc 584 . 2 (πœ‘ β†’ βˆƒπ‘£ ∈ 𝒫 𝐴(𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹)
198 reseq2 5976 . . . 4 (𝑣 = π‘₯ β†’ (𝐹 β†Ύ 𝑣) = (𝐹 β†Ύ π‘₯))
199 id 22 . . . 4 (𝑣 = π‘₯ β†’ 𝑣 = π‘₯)
200 eqidd 2733 . . . 4 (𝑣 = π‘₯ β†’ ran 𝐹 = ran 𝐹)
201198, 199, 200f1oeq123d 6827 . . 3 (𝑣 = π‘₯ β†’ ((𝐹 β†Ύ 𝑣):𝑣–1-1-ontoβ†’ran 𝐹 ↔ (𝐹 β†Ύ π‘₯):π‘₯–1-1-ontoβ†’ran 𝐹))
202201cbvrexvw 3235 . 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 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  βˆƒ!wreu 3374  Vcvv 3474   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Or wor 5587   We wwe 5630  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“ontoβ†’wfo 6541  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  β„©crio 7366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367
This theorem is referenced by:  wessf1orn  43970
  Copyright terms: Public domain W3C validator