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 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-1wf1 6331  ontowfo 6332  1-1-ontowf1o 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