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

Theorem wessf1ornlem 41749
 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 5927 . . . . . . . 8 (𝐹 “ {𝑢}) ⊆ dom 𝐹
3 wessf1ornlem.f . . . . . . . . . 10 (𝜑𝐹 Fn 𝐴)
43fndmd 6436 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
54adantr 484 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → dom 𝐹 = 𝐴)
62, 5sseqtrid 3994 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ⊆ 𝐴)
7 wessf1ornlem.r . . . . . . . . . 10 (𝜑𝑅 We 𝐴)
87adantr 484 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → 𝑅 We 𝐴)
92, 4sseqtrid 3994 . . . . . . . . . . 11 (𝜑 → (𝐹 “ {𝑢}) ⊆ 𝐴)
101, 9ssexd 5204 . . . . . . . . . 10 (𝜑 → (𝐹 “ {𝑢}) ∈ V)
1110adantr 484 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ∈ V)
12 inisegn0 5939 . . . . . . . . . . 11 (𝑢 ∈ ran 𝐹 ↔ (𝐹 “ {𝑢}) ≠ ∅)
1312biimpi 219 . . . . . . . . . 10 (𝑢 ∈ ran 𝐹 → (𝐹 “ {𝑢}) ≠ ∅)
1413adantl 485 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ≠ ∅)
15 wereu 5528 . . . . . . . . 9 ((𝑅 We 𝐴 ∧ ((𝐹 “ {𝑢}) ∈ V ∧ (𝐹 “ {𝑢}) ⊆ 𝐴 ∧ (𝐹 “ {𝑢}) ≠ ∅)) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
168, 11, 6, 14, 15syl13anc 1369 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
17 riotacl 7115 . . . . . . . 8 (∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (𝐹 “ {𝑢}))
1816, 17syl 17 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (𝐹 “ {𝑢}))
196, 18sseldd 3943 . . . . . 6 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
2019ralrimiva 3174 . . . . 5 (𝜑 → ∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
21 wessf1ornlem.g . . . . . . 7 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))
22 sneq 4549 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑦} = {𝑢})
2322imaeq2d 5907 . . . . . . . . . 10 (𝑦 = 𝑢 → (𝐹 “ {𝑦}) = (𝐹 “ {𝑢}))
2423raleqdv 3392 . . . . . . . . . 10 (𝑦 = 𝑢 → (∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
2523, 24riotaeqbidv 7101 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
26 breq1 5045 . . . . . . . . . . . . 13 (𝑧 = 𝑡 → (𝑧𝑅𝑥𝑡𝑅𝑥))
2726notbid 321 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑡𝑅𝑥))
2827cbvralvw 3424 . . . . . . . . . . 11 (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥)
29 breq2 5046 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑡𝑅𝑥𝑡𝑅𝑣))
3029notbid 321 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (¬ 𝑡𝑅𝑥 ↔ ¬ 𝑡𝑅𝑣))
3130ralbidv 3187 . . . . . . . . . . 11 (𝑥 = 𝑣 → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3228, 31syl5bb 286 . . . . . . . . . 10 (𝑥 = 𝑣 → (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3332cbvriotavw 7108 . . . . . . . . 9 (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
3425, 33syl6eq 2873 . . . . . . . 8 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3534cbvmptv 5145 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↦ (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) = (𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3621, 35eqtri 2845 . . . . . 6 𝐺 = (𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3736rnmptss 6868 . . . . 5 (∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴 → ran 𝐺𝐴)
3820, 37syl 17 . . . 4 (𝜑 → ran 𝐺𝐴)
391, 38sselpwd 5206 . . 3 (𝜑 → ran 𝐺 ∈ 𝒫 𝐴)
40 dffn3 6506 . . . . . . 7 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
413, 40sylib 221 . . . . . 6 (𝜑𝐹:𝐴⟶ran 𝐹)
4241, 38fssresd 6526 . . . . 5 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹)
43 fvres 6671 . . . . . . . . . . . . 13 (𝑤 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑤) = (𝐹𝑤))
4443eqcomd 2828 . . . . . . . . . . . 12 (𝑤 ∈ ran 𝐺 → (𝐹𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
4544ad2antrr 725 . . . . . . . . . . 11 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
46 simpr 488 . . . . . . . . . . 11 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡))
47 fvres 6671 . . . . . . . . . . . 12 (𝑡 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹𝑡))
4847ad2antlr 726 . . . . . . . . . . 11 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹𝑡))
4945, 46, 483eqtrd 2861 . . . . . . . . . 10 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = (𝐹𝑡))
50493adantl1 1163 . . . . . . . . 9 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = (𝐹𝑡))
51 simpl1 1188 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝜑)
52 simpl3 1190 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑡 ∈ ran 𝐺)
53 simpl2 1189 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤 ∈ ran 𝐺)
54 id 22 . . . . . . . . . . . . 13 ((𝐹𝑤) = (𝐹𝑡) → (𝐹𝑤) = (𝐹𝑡))
5554eqcomd 2828 . . . . . . . . . . . 12 ((𝐹𝑤) = (𝐹𝑡) → (𝐹𝑡) = (𝐹𝑤))
5655adantl 485 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝐹𝑡) = (𝐹𝑤))
57 eleq1w 2896 . . . . . . . . . . . . . . 15 (𝑏 = 𝑤 → (𝑏 ∈ ran 𝐺𝑤 ∈ ran 𝐺))
58573anbi3d 1439 . . . . . . . . . . . . . 14 (𝑏 = 𝑤 → ((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ↔ (𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺)))
59 fveq2 6652 . . . . . . . . . . . . . . 15 (𝑏 = 𝑤 → (𝐹𝑏) = (𝐹𝑤))
6059eqeq2d 2833 . . . . . . . . . . . . . 14 (𝑏 = 𝑤 → ((𝐹𝑡) = (𝐹𝑏) ↔ (𝐹𝑡) = (𝐹𝑤)))
6158, 60anbi12d 633 . . . . . . . . . . . . 13 (𝑏 = 𝑤 → (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) ↔ ((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤))))
62 breq1 5045 . . . . . . . . . . . . . 14 (𝑏 = 𝑤 → (𝑏𝑅𝑡𝑤𝑅𝑡))
6362notbid 321 . . . . . . . . . . . . 13 (𝑏 = 𝑤 → (¬ 𝑏𝑅𝑡 ↔ ¬ 𝑤𝑅𝑡))
6461, 63imbi12d 348 . . . . . . . . . . . 12 (𝑏 = 𝑤 → ((((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡) ↔ (((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤)) → ¬ 𝑤𝑅𝑡)))
65 eleq1w 2896 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑡 → (𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺))
66653anbi2d 1438 . . . . . . . . . . . . . . 15 (𝑎 = 𝑡 → ((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ↔ (𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺)))
67 fveqeq2 6661 . . . . . . . . . . . . . . 15 (𝑎 = 𝑡 → ((𝐹𝑎) = (𝐹𝑏) ↔ (𝐹𝑡) = (𝐹𝑏)))
6866, 67anbi12d 633 . . . . . . . . . . . . . 14 (𝑎 = 𝑡 → (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) ↔ ((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏))))
69 breq2 5046 . . . . . . . . . . . . . . 15 (𝑎 = 𝑡 → (𝑏𝑅𝑎𝑏𝑅𝑡))
7069notbid 321 . . . . . . . . . . . . . 14 (𝑎 = 𝑡 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑏𝑅𝑡))
7168, 70imbi12d 348 . . . . . . . . . . . . 13 (𝑎 = 𝑡 → ((((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎) ↔ (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡)))
72 eleq1w 2896 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑏 → (𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺))
73723anbi3d 1439 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑏 → ((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ↔ (𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺)))
74 fveq2 6652 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑏 → (𝐹𝑡) = (𝐹𝑏))
7574eqeq2d 2833 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑏 → ((𝐹𝑎) = (𝐹𝑡) ↔ (𝐹𝑎) = (𝐹𝑏)))
7673, 75anbi12d 633 . . . . . . . . . . . . . . 15 (𝑡 = 𝑏 → (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) ↔ ((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏))))
77 breq1 5045 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑏 → (𝑡𝑅𝑎𝑏𝑅𝑎))
7877notbid 321 . . . . . . . . . . . . . . 15 (𝑡 = 𝑏 → (¬ 𝑡𝑅𝑎 ↔ ¬ 𝑏𝑅𝑎))
7976, 78imbi12d 348 . . . . . . . . . . . . . 14 (𝑡 = 𝑏 → ((((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎) ↔ (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎)))
80 eleq1w 2896 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑎 → (𝑤 ∈ ran 𝐺𝑎 ∈ ran 𝐺))
81803anbi2d 1438 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑎 → ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ↔ (𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺)))
82 fveqeq2 6661 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑎 → ((𝐹𝑤) = (𝐹𝑡) ↔ (𝐹𝑎) = (𝐹𝑡)))
8381, 82anbi12d 633 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑎 → (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ↔ ((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡))))
84 breq2 5046 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑎 → (𝑡𝑅𝑤𝑡𝑅𝑎))
8584notbid 321 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑎 → (¬ 𝑡𝑅𝑤 ↔ ¬ 𝑡𝑅𝑎))
8683, 85imbi12d 348 . . . . . . . . . . . . . . 15 (𝑤 = 𝑎 → ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑤) ↔ (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎)))
8736elrnmpt 5805 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ V → (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)))
8887elv 3474 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
8988biimpi 219 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ran 𝐺 → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
9089adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ran 𝐺 ∧ (𝐹𝑤) = (𝐹𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
91903ad2antl2 1183 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
92 simp3 1135 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
9392eqcomd 2828 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)
94 simp11 1200 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝜑)
95 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
96 breq2 5046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑤 → (𝑡𝑅𝑣𝑡𝑅𝑤))
9796notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑤 → (¬ 𝑡𝑅𝑣 ↔ ¬ 𝑡𝑅𝑤))
9897ralbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = 𝑤 → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
9998cbvriotavw 7108 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
10095, 99syl6req 2874 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
1011003ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
10298cbvreuvw 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
10316, 102sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ ran 𝐹) → ∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
104 riota1 7119 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ ran 𝐹) → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
1061053adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
107101, 106mpbird 260 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
108107simpld 498 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (𝐹 “ {𝑢}))
10994, 108syld3an1 1407 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (𝐹 “ {𝑢}))
110 simp2 1134 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑢 ∈ ran 𝐹)
11194, 110, 16syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
11298riota2 7123 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
113109, 111, 112syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
11493, 113mpbird 260 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
1151143adant1r 1174 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
11638sselda 3942 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ran 𝐺) → 𝑡𝐴)
1171163adant2 1128 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → 𝑡𝐴)
118117adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑡𝐴)
1191183ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡𝐴)
12055ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝐹𝑡) = (𝐹𝑤))
1211203adant3 1129 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑡) = (𝐹𝑤))
122 fniniseg 6812 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 Fn 𝐴 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
12394, 3, 1223syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
124109, 123mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢))
125124simprd 499 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑤) = 𝑢)
1261253adant1r 1174 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑤) = 𝑢)
127121, 126eqtrd 2857 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑡) = 𝑢)
128 fniniseg 6812 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝐴 → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1293, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1301293ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
131130ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1321313adant3 1129 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
133119, 127, 132mpbir2and 712 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ (𝐹 “ {𝑢}))
134 rspa 3196 . . . . . . . . . . . . . . . . . 18 ((∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤𝑡 ∈ (𝐹 “ {𝑢})) → ¬ 𝑡𝑅𝑤)
135115, 133, 134syl2anc 587 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ¬ 𝑡𝑅𝑤)
136135rexlimdv3a 3272 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤))
13791, 136mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑤)
13886, 137chvarvv 2005 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎)
13979, 138chvarvv 2005 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎)
14071, 139chvarvv 2005 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡)
14164, 140chvarvv 2005 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤)) → ¬ 𝑤𝑅𝑡)
14251, 52, 53, 56, 141syl31anc 1370 . . . . . . . . . 10 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑤𝑅𝑡)
143 weso 5523 . . . . . . . . . . . . . 14 (𝑅 We 𝐴𝑅 Or 𝐴)
1447, 143syl 17 . . . . . . . . . . . . 13 (𝜑𝑅 Or 𝐴)
145144adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑅 Or 𝐴)
1461453ad2antl1 1182 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑅 Or 𝐴)
14738sselda 3942 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐺) → 𝑤𝐴)
1481473adant3 1129 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → 𝑤𝐴)
149148adantr 484 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤𝐴)
150 sotrieq2 5480 . . . . . . . . . . 11 ((𝑅 Or 𝐴 ∧ (𝑤𝐴𝑡𝐴)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
151146, 149, 118, 150syl12anc 835 . . . . . . . . . 10 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
152142, 137, 151mpbir2and 712 . . . . . . . . 9 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤 = 𝑡)
15350, 152syldan 594 . . . . . . . 8 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → 𝑤 = 𝑡)
154153ex 416 . . . . . . 7 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
1551543expb 1117 . . . . . 6 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
156155ralrimivva 3181 . . . . 5 (𝜑 → ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
157 dff13 6996 . . . . 5 ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
15842, 156, 157sylanbrc 586 . . . 4 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹)
159 riotaex 7102 . . . . . . . . . . 11 (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
160159rgenw 3142 . . . . . . . . . 10 𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
16136fnmpt 6468 . . . . . . . . . 10 (∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V → 𝐺 Fn ran 𝐹)
162160, 161mp1i 13 . . . . . . . . 9 (𝜑𝐺 Fn ran 𝐹)
163 dffn3 6506 . . . . . . . . 9 (𝐺 Fn ran 𝐹𝐺:ran 𝐹⟶ran 𝐺)
164162, 163sylib 221 . . . . . . . 8 (𝜑𝐺:ran 𝐹⟶ran 𝐺)
165164ffvelrnda 6833 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) ∈ ran 𝐺)
166165fvresd 6672 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)) = (𝐹‘(𝐺𝑢)))
167 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹)
168159a1i 11 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
16921, 34, 167, 168fvmptd3 6773 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
170169, 18eqeltrd 2914 . . . . . . . . . 10 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) ∈ (𝐹 “ {𝑢}))
171 fvex 6665 . . . . . . . . . . . 12 (𝐺𝑢) ∈ V
172 eleq1 2901 . . . . . . . . . . . . . 14 (𝑤 = (𝐺𝑢) → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝐺𝑢) ∈ (𝐹 “ {𝑢})))
173 eleq1 2901 . . . . . . . . . . . . . . 15 (𝑤 = (𝐺𝑢) → (𝑤𝐴 ↔ (𝐺𝑢) ∈ 𝐴))
174 fveqeq2 6661 . . . . . . . . . . . . . . 15 (𝑤 = (𝐺𝑢) → ((𝐹𝑤) = 𝑢 ↔ (𝐹‘(𝐺𝑢)) = 𝑢))
175173, 174anbi12d 633 . . . . . . . . . . . . . 14 (𝑤 = (𝐺𝑢) → ((𝑤𝐴 ∧ (𝐹𝑤) = 𝑢) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
176172, 175bibi12d 349 . . . . . . . . . . . . 13 (𝑤 = (𝐺𝑢) → ((𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)) ↔ ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢))))
177176imbi2d 344 . . . . . . . . . . . 12 (𝑤 = (𝐺𝑢) → ((𝜑 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢))) ↔ (𝜑 → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))))
1783, 122syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
179171, 177, 178vtocl 3534 . . . . . . . . . . 11 (𝜑 → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
180179adantr 484 . . . . . . . . . 10 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
181170, 180mpbid 235 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢))
182181simprd 499 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹‘(𝐺𝑢)) = 𝑢)
183166, 182eqtr2d 2858 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)))
184 fveq2 6652 . . . . . . . 8 (𝑤 = (𝐺𝑢) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)))
185184rspceeqv 3613 . . . . . . 7 (((𝐺𝑢) ∈ ran 𝐺𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢))) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
186165, 183, 185syl2anc 587 . . . . . 6 ((𝜑𝑢 ∈ ran 𝐹) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
187186ralrimiva 3174 . . . . 5 (𝜑 → ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
188 dffo3 6850 . . . . 5 ((𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
18942, 187, 188sylanbrc 586 . . . 4 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹)
190 df-f1o 6341 . . . 4 ((𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹))
191158, 189, 190sylanbrc 586 . . 3 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹)
192 reseq2 5826 . . . . 5 (𝑣 = ran 𝐺 → (𝐹𝑣) = (𝐹 ↾ ran 𝐺))
193 id 22 . . . . 5 (𝑣 = ran 𝐺𝑣 = ran 𝐺)
194 eqidd 2823 . . . . 5 (𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹)
195192, 193, 194f1oeq123d 6592 . . . 4 (𝑣 = ran 𝐺 → ((𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹))
196195rspcev 3598 . . 3 ((ran 𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹) → ∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹)
19739, 191, 196syl2anc 587 . 2 (𝜑 → ∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹)
198 reseq2 5826 . . . 4 (𝑣 = 𝑥 → (𝐹𝑣) = (𝐹𝑥))
199 id 22 . . . 4 (𝑣 = 𝑥𝑣 = 𝑥)
200 eqidd 2823 . . . 4 (𝑣 = 𝑥 → ran 𝐹 = ran 𝐹)
201198, 199, 200f1oeq123d 6592 . . 3 (𝑣 = 𝑥 → ((𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ (𝐹𝑥):𝑥1-1-onto→ran 𝐹))
202201cbvrexvw 3425 . 2 (∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ ∃𝑥 ∈ 𝒫 𝐴(𝐹𝑥):𝑥1-1-onto→ran 𝐹)
203197, 202sylib 221 1 (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹𝑥):𝑥1-1-onto→ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2114   ≠ wne 3011  ∀wral 3130  ∃wrex 3131  ∃!wreu 3132  Vcvv 3469   ⊆ wss 3908  ∅c0 4265  𝒫 cpw 4511  {csn 4539   class class class wbr 5042   ↦ cmpt 5122   Or wor 5450   We wwe 5490  ◡ccnv 5531  dom cdm 5532  ran crn 5533   ↾ cres 5534   “ cima 5535   Fn wfn 6329  ⟶wf 6330  –1-1→wf1 6331  –onto→wfo 6332  –1-1-onto→wf1o 6333  ‘cfv 6334  ℩crio 7097 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098 This theorem is referenced by:  wessf1orn  41750
 Copyright terms: Public domain W3C validator