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

Theorem wessf1ornlem 39888
 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 cnvimass 5643 . . . . . . . . 9 (𝐹 “ {𝑢}) ⊆ dom 𝐹
21a1i 11 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ⊆ dom 𝐹)
3 wessf1ornlem.f . . . . . . . . . 10 (𝜑𝐹 Fn 𝐴)
4 fndm 6151 . . . . . . . . . 10 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
53, 4syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
65adantr 472 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → dom 𝐹 = 𝐴)
72, 6sseqtrd 3782 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ⊆ 𝐴)
8 wessf1ornlem.r . . . . . . . . . 10 (𝜑𝑅 We 𝐴)
98adantr 472 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → 𝑅 We 𝐴)
101, 5syl5sseq 3794 . . . . . . . . . . 11 (𝜑 → (𝐹 “ {𝑢}) ⊆ 𝐴)
11 wessf1ornlem.a . . . . . . . . . . 11 (𝜑𝐴𝑉)
12 ssexg 4956 . . . . . . . . . . 11 (((𝐹 “ {𝑢}) ⊆ 𝐴𝐴𝑉) → (𝐹 “ {𝑢}) ∈ V)
1310, 11, 12syl2anc 696 . . . . . . . . . 10 (𝜑 → (𝐹 “ {𝑢}) ∈ V)
1413adantr 472 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ∈ V)
15 inisegn0 5655 . . . . . . . . . . 11 (𝑢 ∈ ran 𝐹 ↔ (𝐹 “ {𝑢}) ≠ ∅)
1615biimpi 206 . . . . . . . . . 10 (𝑢 ∈ ran 𝐹 → (𝐹 “ {𝑢}) ≠ ∅)
1716adantl 473 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ≠ ∅)
18 wereu 5262 . . . . . . . . 9 ((𝑅 We 𝐴 ∧ ((𝐹 “ {𝑢}) ∈ V ∧ (𝐹 “ {𝑢}) ⊆ 𝐴 ∧ (𝐹 “ {𝑢}) ≠ ∅)) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
199, 14, 7, 17, 18syl13anc 1479 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
20 riotacl 6789 . . . . . . . 8 (∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (𝐹 “ {𝑢}))
2119, 20syl 17 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (𝐹 “ {𝑢}))
227, 21sseldd 3745 . . . . . 6 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
2322ralrimiva 3104 . . . . 5 (𝜑 → ∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
24 wessf1ornlem.g . . . . . . 7 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))
25 sneq 4331 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑦} = {𝑢})
2625imaeq2d 5624 . . . . . . . . . 10 (𝑦 = 𝑢 → (𝐹 “ {𝑦}) = (𝐹 “ {𝑢}))
2726raleqdv 3283 . . . . . . . . . 10 (𝑦 = 𝑢 → (∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
2826, 27riotaeqbidv 6778 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
29 breq1 4807 . . . . . . . . . . . . . . 15 (𝑧 = 𝑡 → (𝑧𝑅𝑥𝑡𝑅𝑥))
3029notbid 307 . . . . . . . . . . . . . 14 (𝑧 = 𝑡 → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑡𝑅𝑥))
3130cbvralv 3310 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥)
3231a1i 11 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥))
33 breq2 4808 . . . . . . . . . . . . . 14 (𝑥 = 𝑣 → (𝑡𝑅𝑥𝑡𝑅𝑣))
3433notbid 307 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (¬ 𝑡𝑅𝑥 ↔ ¬ 𝑡𝑅𝑣))
3534ralbidv 3124 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3632, 35bitrd 268 . . . . . . . . . . 11 (𝑥 = 𝑣 → (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3736cbvriotav 6786 . . . . . . . . . 10 (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
3837a1i 11 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3928, 38eqtrd 2794 . . . . . . . 8 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4039cbvmptv 4902 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↦ (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) = (𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4124, 40eqtri 2782 . . . . . 6 𝐺 = (𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4241rnmptss 6556 . . . . 5 (∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴 → ran 𝐺𝐴)
4323, 42syl 17 . . . 4 (𝜑 → ran 𝐺𝐴)
4411, 43ssexd 4957 . . . . 5 (𝜑 → ran 𝐺 ∈ V)
45 elpwg 4310 . . . . 5 (ran 𝐺 ∈ V → (ran 𝐺 ∈ 𝒫 𝐴 ↔ ran 𝐺𝐴))
4644, 45syl 17 . . . 4 (𝜑 → (ran 𝐺 ∈ 𝒫 𝐴 ↔ ran 𝐺𝐴))
4743, 46mpbird 247 . . 3 (𝜑 → ran 𝐺 ∈ 𝒫 𝐴)
48 dffn3 6215 . . . . . . . . . 10 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
4948biimpi 206 . . . . . . . . 9 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
503, 49syl 17 . . . . . . . 8 (𝜑𝐹:𝐴⟶ran 𝐹)
5150, 43fssresd 6232 . . . . . . 7 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹)
52 simpl 474 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝜑)
53 simprl 811 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝑤 ∈ ran 𝐺)
54 simprr 813 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝑡 ∈ ran 𝐺)
55 simpl 474 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺))
56 fvres 6369 . . . . . . . . . . . . . . 15 (𝑤 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑤) = (𝐹𝑤))
5756eqcomd 2766 . . . . . . . . . . . . . 14 (𝑤 ∈ ran 𝐺 → (𝐹𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
5857ad2antrr 764 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
59 simpr 479 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡))
60 fvres 6369 . . . . . . . . . . . . . 14 (𝑡 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹𝑡))
6160ad2antlr 765 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹𝑡))
6258, 59, 613eqtrd 2798 . . . . . . . . . . . 12 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = (𝐹𝑡))
63623adantl1 1172 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = (𝐹𝑡))
64 simpl1 1228 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝜑)
65 simpl3 1232 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑡 ∈ ran 𝐺)
66 vex 3343 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ V
6741elrnmpt 5527 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ V → (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
6968biimpi 206 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ran 𝐺 → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
7069adantr 472 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ran 𝐺 ∧ (𝐹𝑤) = (𝐹𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
71703ad2antl2 1202 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
7271, 68sylibr 224 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤 ∈ ran 𝐺)
73 id 22 . . . . . . . . . . . . . . . 16 ((𝐹𝑤) = (𝐹𝑡) → (𝐹𝑤) = (𝐹𝑡))
7473eqcomd 2766 . . . . . . . . . . . . . . 15 ((𝐹𝑤) = (𝐹𝑡) → (𝐹𝑡) = (𝐹𝑤))
7574adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝐹𝑡) = (𝐹𝑤))
76 eleq1w 2822 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → (𝑏 ∈ ran 𝐺𝑤 ∈ ran 𝐺))
77763anbi3d 1554 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → ((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ↔ (𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺)))
78 fveq2 6353 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → (𝐹𝑏) = (𝐹𝑤))
7978eqeq2d 2770 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → ((𝐹𝑡) = (𝐹𝑏) ↔ (𝐹𝑡) = (𝐹𝑤)))
8077, 79anbi12d 749 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) ↔ ((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤))))
81 breq1 4807 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → (𝑏𝑅𝑡𝑤𝑅𝑡))
8281notbid 307 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (¬ 𝑏𝑅𝑡 ↔ ¬ 𝑤𝑅𝑡))
8380, 82imbi12d 333 . . . . . . . . . . . . . . 15 (𝑏 = 𝑤 → ((((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡) ↔ (((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤)) → ¬ 𝑤𝑅𝑡)))
84 eleq1w 2822 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑡 → (𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺))
85843anbi2d 1553 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → ((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ↔ (𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺)))
86 fveq2 6353 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑡 → (𝐹𝑎) = (𝐹𝑡))
8786eqeq1d 2762 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → ((𝐹𝑎) = (𝐹𝑏) ↔ (𝐹𝑡) = (𝐹𝑏)))
8885, 87anbi12d 749 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑡 → (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) ↔ ((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏))))
89 breq2 4808 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → (𝑏𝑅𝑎𝑏𝑅𝑡))
9089notbid 307 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑡 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑏𝑅𝑡))
9188, 90imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑡 → ((((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎) ↔ (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡)))
92 eleq1w 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺))
93923anbi3d 1554 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ↔ (𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺)))
94 fveq2 6353 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝐹𝑡) = (𝐹𝑏))
9594eqeq2d 2770 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝐹𝑎) = (𝐹𝑡) ↔ (𝐹𝑎) = (𝐹𝑏)))
9693, 95anbi12d 749 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) ↔ ((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏))))
97 breq1 4807 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → (𝑡𝑅𝑎𝑏𝑅𝑎))
9897notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → (¬ 𝑡𝑅𝑎 ↔ ¬ 𝑏𝑅𝑎))
9996, 98imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑏 → ((((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎) ↔ (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎)))
100 eleq1w 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑎 → (𝑤 ∈ ran 𝐺𝑎 ∈ ran 𝐺))
1011003anbi2d 1553 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ↔ (𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺)))
102 fveq2 6353 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑎 → (𝐹𝑤) = (𝐹𝑎))
103102eqeq1d 2762 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → ((𝐹𝑤) = (𝐹𝑡) ↔ (𝐹𝑎) = (𝐹𝑡)))
104101, 103anbi12d 749 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑎 → (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ↔ ((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡))))
105 breq2 4808 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → (𝑡𝑅𝑤𝑡𝑅𝑎))
106105notbid 307 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑎 → (¬ 𝑡𝑅𝑤 ↔ ¬ 𝑡𝑅𝑎))
107104, 106imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑎 → ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑤) ↔ (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎)))
108 nfv 1992 . . . . . . . . . . . . . . . . . . . . . 22 𝑢𝜑
109 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . 23 𝑢𝑤
110 nfmpt1 4899 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑢(𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
11141, 110nfcxfr 2900 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑢𝐺
112111nfrn 5523 . . . . . . . . . . . . . . . . . . . . . . 23 𝑢ran 𝐺
113109, 112nfel 2915 . . . . . . . . . . . . . . . . . . . . . 22 𝑢 𝑤 ∈ ran 𝐺
114112nfcri 2896 . . . . . . . . . . . . . . . . . . . . . 22 𝑢 𝑡 ∈ ran 𝐺
115108, 113, 114nf3an 1980 . . . . . . . . . . . . . . . . . . . . 21 𝑢(𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)
116 nfv 1992 . . . . . . . . . . . . . . . . . . . . 21 𝑢(𝐹𝑤) = (𝐹𝑡)
117115, 116nfan 1977 . . . . . . . . . . . . . . . . . . . 20 𝑢((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡))
118 nfv 1992 . . . . . . . . . . . . . . . . . . . 20 𝑢 ¬ 𝑡𝑅𝑤
119 simp3 1133 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
120119eqcomd 2766 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)
121 simp11 1246 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝜑)
122 simp2 1132 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑢 ∈ ran 𝐹)
123 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
124 breq2 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = 𝑤 → (𝑡𝑅𝑣𝑡𝑅𝑤))
125124notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑤 → (¬ 𝑡𝑅𝑣 ↔ ¬ 𝑡𝑅𝑤))
126125ralbidv 3124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 = 𝑤 → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
127126cbvriotav 6786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
128127a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
129123, 128eqtr2d 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
1301293ad2ant3 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
131126cbvreuv 3312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
13219, 131sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ ran 𝐹) → ∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
133 riota1 6793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ ran 𝐹) → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
1351343adant3 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
136130, 135mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
137136simpld 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (𝐹 “ {𝑢}))
138121, 122, 119, 137syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (𝐹 “ {𝑢}))
139121, 122, 19syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
140126riota2 6797 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
141138, 139, 140syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
142120, 141mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
1431423adant1r 1188 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
14443sselda 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑡 ∈ ran 𝐺) → 𝑡𝐴)
1451443adant2 1126 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → 𝑡𝐴)
146145adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑡𝐴)
1471463ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡𝐴)
14874ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝐹𝑡) = (𝐹𝑤))
1491483adant3 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑡) = (𝐹𝑤))
150 fniniseg 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 Fn 𝐴 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
151121, 3, 1503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
152138, 151mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢))
153152simprd 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑤) = 𝑢)
1541533adant1r 1188 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑤) = 𝑢)
155149, 154eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑡) = 𝑢)
156147, 155jca 555 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢))
157 fniniseg 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 Fn 𝐴 → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1583, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1591583ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
160159ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1611603adant3 1127 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
162156, 161mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ (𝐹 “ {𝑢}))
163 rspa 3068 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤𝑡 ∈ (𝐹 “ {𝑢})) → ¬ 𝑡𝑅𝑤)
164143, 162, 163syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ¬ 𝑡𝑅𝑤)
1651643exp 1113 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝑢 ∈ ran 𝐹 → (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤)))
166117, 118, 165rexlimd 3164 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤))
16771, 166mpd 15 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑤)
168107, 167chvarv 2408 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎)
16999, 168chvarv 2408 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎)
17091, 169chvarv 2408 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡)
17183, 170chvarv 2408 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤)) → ¬ 𝑤𝑅𝑡)
17264, 65, 72, 75, 171syl31anc 1480 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑤𝑅𝑡)
173172, 167jca 555 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤))
174 weso 5257 . . . . . . . . . . . . . . . 16 (𝑅 We 𝐴𝑅 Or 𝐴)
1758, 174syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑅 Or 𝐴)
176175adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑅 Or 𝐴)
1771763ad2antl1 1201 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑅 Or 𝐴)
17843sselda 3744 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ran 𝐺) → 𝑤𝐴)
1791783adant3 1127 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → 𝑤𝐴)
180179adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤𝐴)
181 sotrieq2 5215 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴 ∧ (𝑤𝐴𝑡𝐴)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
182177, 180, 146, 181syl12anc 1475 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
183173, 182mpbird 247 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤 = 𝑡)
18455, 63, 183syl2anc 696 . . . . . . . . . 10 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → 𝑤 = 𝑡)
185184ex 449 . . . . . . . . 9 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
18652, 53, 54, 185syl3anc 1477 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
187186ralrimivva 3109 . . . . . . 7 (𝜑 → ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
18851, 187jca 555 . . . . . 6 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
189 dff13 6676 . . . . . 6 ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
190188, 189sylibr 224 . . . . 5 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹)
191 riotaex 6779 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
192191rgenw 3062 . . . . . . . . . . . . 13 𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
193192a1i 11 . . . . . . . . . . . 12 (𝜑 → ∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
19441fnmpt 6181 . . . . . . . . . . . 12 (∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V → 𝐺 Fn ran 𝐹)
195193, 194syl 17 . . . . . . . . . . 11 (𝜑𝐺 Fn ran 𝐹)
196 dffn3 6215 . . . . . . . . . . . 12 (𝐺 Fn ran 𝐹𝐺:ran 𝐹⟶ran 𝐺)
197196biimpi 206 . . . . . . . . . . 11 (𝐺 Fn ran 𝐹𝐺:ran 𝐹⟶ran 𝐺)
198195, 197syl 17 . . . . . . . . . 10 (𝜑𝐺:ran 𝐹⟶ran 𝐺)
199198ffvelrnda 6523 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) ∈ ran 𝐺)
200 fvres 6369 . . . . . . . . . . 11 ((𝐺𝑢) ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)) = (𝐹‘(𝐺𝑢)))
201199, 200syl 17 . . . . . . . . . 10 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)) = (𝐹‘(𝐺𝑢)))
20217, 15sylibr 224 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹)
203191a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
20441fvmpt2 6454 . . . . . . . . . . . . . 14 ((𝑢 ∈ ran 𝐹 ∧ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V) → (𝐺𝑢) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
205202, 203, 204syl2anc 696 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
206205, 21eqeltrd 2839 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) ∈ (𝐹 “ {𝑢}))
207 fvex 6363 . . . . . . . . . . . . . 14 (𝐺𝑢) ∈ V
208 eleq1 2827 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐺𝑢) → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝐺𝑢) ∈ (𝐹 “ {𝑢})))
209 eleq1 2827 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐺𝑢) → (𝑤𝐴 ↔ (𝐺𝑢) ∈ 𝐴))
210 fveq2 6353 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐺𝑢) → (𝐹𝑤) = (𝐹‘(𝐺𝑢)))
211210eqeq1d 2762 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐺𝑢) → ((𝐹𝑤) = 𝑢 ↔ (𝐹‘(𝐺𝑢)) = 𝑢))
212209, 211anbi12d 749 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐺𝑢) → ((𝑤𝐴 ∧ (𝐹𝑤) = 𝑢) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
213208, 212bibi12d 334 . . . . . . . . . . . . . . 15 (𝑤 = (𝐺𝑢) → ((𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)) ↔ ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢))))
214213imbi2d 329 . . . . . . . . . . . . . 14 (𝑤 = (𝐺𝑢) → ((𝜑 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢))) ↔ (𝜑 → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))))
2153, 150syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
216207, 214, 215vtocl 3399 . . . . . . . . . . . . 13 (𝜑 → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
217216adantr 472 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
218206, 217mpbid 222 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢))
219218simprd 482 . . . . . . . . . 10 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹‘(𝐺𝑢)) = 𝑢)
220201, 219eqtr2d 2795 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)))
221 fveq2 6353 . . . . . . . . . . 11 (𝑤 = (𝐺𝑢) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)))
222221eqeq2d 2770 . . . . . . . . . 10 (𝑤 = (𝐺𝑢) → (𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤) ↔ 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢))))
223222rspcev 3449 . . . . . . . . 9 (((𝐺𝑢) ∈ ran 𝐺𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢))) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
224199, 220, 223syl2anc 696 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
225224ralrimiva 3104 . . . . . . 7 (𝜑 → ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
22651, 225jca 555 . . . . . 6 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
227 dffo3 6538 . . . . . 6 ((𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
228226, 227sylibr 224 . . . . 5 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹)
229190, 228jca 555 . . . 4 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹))
230 df-f1o 6056 . . . 4 ((𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹))
231229, 230sylibr 224 . . 3 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹)
232 nfcv 2902 . . . . . 6 𝑣𝐹
233 nfcv 2902 . . . . . . . . 9 𝑣ran 𝐹
234 nfriota1 6782 . . . . . . . . 9 𝑣(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
235233, 234nfmpt 4898 . . . . . . . 8 𝑣(𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
23641, 235nfcxfr 2900 . . . . . . 7 𝑣𝐺
237236nfrn 5523 . . . . . 6 𝑣ran 𝐺
238232, 237nfres 5553 . . . . 5 𝑣(𝐹 ↾ ran 𝐺)
239238, 237, 233nff1o 6297 . . . 4 𝑣(𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹
240 reseq2 5546 . . . . 5 (𝑣 = ran 𝐺 → (𝐹𝑣) = (𝐹 ↾ ran 𝐺))
241 id 22 . . . . 5 (𝑣 = ran 𝐺𝑣 = ran 𝐺)
242 eqidd 2761 . . . . 5 (𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹)
243240, 241, 242f1oeq123d 6295 . . . 4 (𝑣 = ran 𝐺 → ((𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹))
244239, 243rspce 3444 . . 3 ((ran 𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹) → ∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹)
24547, 231, 244syl2anc 696 . 2 (𝜑 → ∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹)
246 reseq2 5546 . . . 4 (𝑣 = 𝑥 → (𝐹𝑣) = (𝐹𝑥))
247 id 22 . . . 4 (𝑣 = 𝑥𝑣 = 𝑥)
248 eqidd 2761 . . . 4 (𝑣 = 𝑥 → ran 𝐹 = ran 𝐹)
249246, 247, 248f1oeq123d 6295 . . 3 (𝑣 = 𝑥 → ((𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ (𝐹𝑥):𝑥1-1-onto→ran 𝐹))
250249cbvrexv 3311 . 2 (∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ ∃𝑥 ∈ 𝒫 𝐴(𝐹𝑥):𝑥1-1-onto→ran 𝐹)
251245, 250sylib 208 1 (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹𝑥):𝑥1-1-onto→ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051  ∃!wreu 3052  Vcvv 3340   ⊆ wss 3715  ∅c0 4058  𝒫 cpw 4302  {csn 4321   class class class wbr 4804   ↦ cmpt 4881   Or wor 5186   We wwe 5224  ◡ccnv 5265  dom cdm 5266  ran crn 5267   ↾ cres 5268   “ cima 5269   Fn wfn 6044  ⟶wf 6045  –1-1→wf1 6046  –onto→wfo 6047  –1-1-onto→wf1o 6048  ‘cfv 6049  ℩crio 6774 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775 This theorem is referenced by:  wessf1orn  39889
 Copyright terms: Public domain W3C validator