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 39685
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 5520 . . . . . . . . 9 (𝐹 “ {𝑢}) ⊆ dom 𝐹
21a1i 11 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ⊆ dom 𝐹)
3 wessf1ornlem.f . . . . . . . . . 10 (𝜑𝐹 Fn 𝐴)
4 fndm 6028 . . . . . . . . . 10 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
53, 4syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
65adantr 480 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → dom 𝐹 = 𝐴)
72, 6sseqtrd 3674 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ⊆ 𝐴)
8 wessf1ornlem.r . . . . . . . . . 10 (𝜑𝑅 We 𝐴)
98adantr 480 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → 𝑅 We 𝐴)
101, 5syl5sseq 3686 . . . . . . . . . . 11 (𝜑 → (𝐹 “ {𝑢}) ⊆ 𝐴)
11 wessf1ornlem.a . . . . . . . . . . 11 (𝜑𝐴𝑉)
12 ssexg 4837 . . . . . . . . . . 11 (((𝐹 “ {𝑢}) ⊆ 𝐴𝐴𝑉) → (𝐹 “ {𝑢}) ∈ V)
1310, 11, 12syl2anc 694 . . . . . . . . . 10 (𝜑 → (𝐹 “ {𝑢}) ∈ V)
1413adantr 480 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ∈ V)
15 inisegn0 5532 . . . . . . . . . . 11 (𝑢 ∈ ran 𝐹 ↔ (𝐹 “ {𝑢}) ≠ ∅)
1615biimpi 206 . . . . . . . . . 10 (𝑢 ∈ ran 𝐹 → (𝐹 “ {𝑢}) ≠ ∅)
1716adantl 481 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ≠ ∅)
18 wereu 5139 . . . . . . . . 9 ((𝑅 We 𝐴 ∧ ((𝐹 “ {𝑢}) ∈ V ∧ (𝐹 “ {𝑢}) ⊆ 𝐴 ∧ (𝐹 “ {𝑢}) ≠ ∅)) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
199, 14, 7, 17, 18syl13anc 1368 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
20 riotacl 6665 . . . . . . . 8 (∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (𝐹 “ {𝑢}))
2119, 20syl 17 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (𝐹 “ {𝑢}))
227, 21sseldd 3637 . . . . . 6 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
2322ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
24 wessf1ornlem.g . . . . . . 7 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))
25 sneq 4220 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑦} = {𝑢})
2625imaeq2d 5501 . . . . . . . . . 10 (𝑦 = 𝑢 → (𝐹 “ {𝑦}) = (𝐹 “ {𝑢}))
2726raleqdv 3174 . . . . . . . . . 10 (𝑦 = 𝑢 → (∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
2826, 27riotaeqbidv 6654 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
29 breq1 4688 . . . . . . . . . . . . . . 15 (𝑧 = 𝑡 → (𝑧𝑅𝑥𝑡𝑅𝑥))
3029notbid 307 . . . . . . . . . . . . . 14 (𝑧 = 𝑡 → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑡𝑅𝑥))
3130cbvralv 3201 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥)
3231a1i 11 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥))
33 breq2 4689 . . . . . . . . . . . . . 14 (𝑥 = 𝑣 → (𝑡𝑅𝑥𝑡𝑅𝑣))
3433notbid 307 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (¬ 𝑡𝑅𝑥 ↔ ¬ 𝑡𝑅𝑣))
3534ralbidv 3015 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3632, 35bitrd 268 . . . . . . . . . . 11 (𝑥 = 𝑣 → (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3736cbvriotav 6662 . . . . . . . . . 10 (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
3837a1i 11 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3928, 38eqtrd 2685 . . . . . . . 8 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4039cbvmptv 4783 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↦ (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) = (𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4124, 40eqtri 2673 . . . . . 6 𝐺 = (𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4241rnmptss 6432 . . . . 5 (∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴 → ran 𝐺𝐴)
4323, 42syl 17 . . . 4 (𝜑 → ran 𝐺𝐴)
4411, 43ssexd 4838 . . . . 5 (𝜑 → ran 𝐺 ∈ V)
45 elpwg 4199 . . . . 5 (ran 𝐺 ∈ V → (ran 𝐺 ∈ 𝒫 𝐴 ↔ ran 𝐺𝐴))
4644, 45syl 17 . . . 4 (𝜑 → (ran 𝐺 ∈ 𝒫 𝐴 ↔ ran 𝐺𝐴))
4743, 46mpbird 247 . . 3 (𝜑 → ran 𝐺 ∈ 𝒫 𝐴)
48 dffn3 6092 . . . . . . . . . 10 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
4948biimpi 206 . . . . . . . . 9 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
503, 49syl 17 . . . . . . . 8 (𝜑𝐹:𝐴⟶ran 𝐹)
5150, 43fssresd 6109 . . . . . . 7 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹)
52 simpl 472 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝜑)
53 simprl 809 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝑤 ∈ ran 𝐺)
54 simprr 811 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝑡 ∈ ran 𝐺)
55 simpl 472 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺))
56 fvres 6245 . . . . . . . . . . . . . . 15 (𝑤 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑤) = (𝐹𝑤))
5756eqcomd 2657 . . . . . . . . . . . . . 14 (𝑤 ∈ ran 𝐺 → (𝐹𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
5857ad2antrr 762 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
59 simpr 476 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡))
60 fvres 6245 . . . . . . . . . . . . . 14 (𝑡 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹𝑡))
6160ad2antlr 763 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹𝑡))
6258, 59, 613eqtrd 2689 . . . . . . . . . . . 12 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = (𝐹𝑡))
63623adantl1 1237 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = (𝐹𝑡))
64 simpl1 1084 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝜑)
65 simpl3 1086 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑡 ∈ ran 𝐺)
66 vex 3234 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ V
6741elrnmpt 5404 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ V → (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
6968biimpi 206 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ran 𝐺 → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
7069adantr 480 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ran 𝐺 ∧ (𝐹𝑤) = (𝐹𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
71703ad2antl2 1244 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
7271, 68sylibr 224 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤 ∈ ran 𝐺)
73 id 22 . . . . . . . . . . . . . . . 16 ((𝐹𝑤) = (𝐹𝑡) → (𝐹𝑤) = (𝐹𝑡))
7473eqcomd 2657 . . . . . . . . . . . . . . 15 ((𝐹𝑤) = (𝐹𝑡) → (𝐹𝑡) = (𝐹𝑤))
7574adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝐹𝑡) = (𝐹𝑤))
76 eleq1 2718 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → (𝑏 ∈ ran 𝐺𝑤 ∈ ran 𝐺))
77763anbi3d 1445 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → ((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ↔ (𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺)))
78 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → (𝐹𝑏) = (𝐹𝑤))
7978eqeq2d 2661 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → ((𝐹𝑡) = (𝐹𝑏) ↔ (𝐹𝑡) = (𝐹𝑤)))
8077, 79anbi12d 747 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) ↔ ((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤))))
81 breq1 4688 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → (𝑏𝑅𝑡𝑤𝑅𝑡))
8281notbid 307 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (¬ 𝑏𝑅𝑡 ↔ ¬ 𝑤𝑅𝑡))
8380, 82imbi12d 333 . . . . . . . . . . . . . . 15 (𝑏 = 𝑤 → ((((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡) ↔ (((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤)) → ¬ 𝑤𝑅𝑡)))
84 eleq1 2718 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑡 → (𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺))
85843anbi2d 1444 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → ((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ↔ (𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺)))
86 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑡 → (𝐹𝑎) = (𝐹𝑡))
8786eqeq1d 2653 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → ((𝐹𝑎) = (𝐹𝑏) ↔ (𝐹𝑡) = (𝐹𝑏)))
8885, 87anbi12d 747 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑡 → (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) ↔ ((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏))))
89 breq2 4689 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → (𝑏𝑅𝑎𝑏𝑅𝑡))
9089notbid 307 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑡 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑏𝑅𝑡))
9188, 90imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑡 → ((((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎) ↔ (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡)))
92 eleq1 2718 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺))
93923anbi3d 1445 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ↔ (𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺)))
94 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝐹𝑡) = (𝐹𝑏))
9594eqeq2d 2661 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝐹𝑎) = (𝐹𝑡) ↔ (𝐹𝑎) = (𝐹𝑏)))
9693, 95anbi12d 747 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) ↔ ((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏))))
97 breq1 4688 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → (𝑡𝑅𝑎𝑏𝑅𝑎))
9897notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → (¬ 𝑡𝑅𝑎 ↔ ¬ 𝑏𝑅𝑎))
9996, 98imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑏 → ((((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎) ↔ (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎)))
100 eleq1 2718 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑎 → (𝑤 ∈ ran 𝐺𝑎 ∈ ran 𝐺))
1011003anbi2d 1444 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ↔ (𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺)))
102 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑎 → (𝐹𝑤) = (𝐹𝑎))
103102eqeq1d 2653 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → ((𝐹𝑤) = (𝐹𝑡) ↔ (𝐹𝑎) = (𝐹𝑡)))
104101, 103anbi12d 747 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑎 → (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ↔ ((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡))))
105 breq2 4689 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → (𝑡𝑅𝑤𝑡𝑅𝑎))
106105notbid 307 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑎 → (¬ 𝑡𝑅𝑤 ↔ ¬ 𝑡𝑅𝑎))
107104, 106imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑎 → ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑤) ↔ (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎)))
108 nfv 1883 . . . . . . . . . . . . . . . . . . . . . 22 𝑢𝜑
109 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . 23 𝑢𝑤
110 nfmpt1 4780 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑢(𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
11141, 110nfcxfr 2791 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑢𝐺
112111nfrn 5400 . . . . . . . . . . . . . . . . . . . . . . 23 𝑢ran 𝐺
113109, 112nfel 2806 . . . . . . . . . . . . . . . . . . . . . 22 𝑢 𝑤 ∈ ran 𝐺
114112nfcri 2787 . . . . . . . . . . . . . . . . . . . . . 22 𝑢 𝑡 ∈ ran 𝐺
115108, 113, 114nf3an 1871 . . . . . . . . . . . . . . . . . . . . 21 𝑢(𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)
116 nfv 1883 . . . . . . . . . . . . . . . . . . . . 21 𝑢(𝐹𝑤) = (𝐹𝑡)
117115, 116nfan 1868 . . . . . . . . . . . . . . . . . . . 20 𝑢((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡))
118 nfv 1883 . . . . . . . . . . . . . . . . . . . 20 𝑢 ¬ 𝑡𝑅𝑤
119 simp3 1083 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
120119eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)
121 simp11 1111 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝜑)
122 simp2 1082 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑢 ∈ ran 𝐹)
123 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
124 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = 𝑤 → (𝑡𝑅𝑣𝑡𝑅𝑤))
125124notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑤 → (¬ 𝑡𝑅𝑣 ↔ ¬ 𝑡𝑅𝑤))
126125ralbidv 3015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 = 𝑤 → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
127126cbvriotav 6662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
128127a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
129123, 128eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
1301293ad2ant3 1104 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
131126cbvreuv 3203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
13219, 131sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ ran 𝐹) → ∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
133 riota1 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ ran 𝐹) → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
1351343adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
136130, 135mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
137136simpld 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (𝐹 “ {𝑢}))
138121, 122, 119, 137syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (𝐹 “ {𝑢}))
139121, 122, 19syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
140126riota2 6673 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
141138, 139, 140syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
142120, 141mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
1431423adant1r 1359 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
14443sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑡 ∈ ran 𝐺) → 𝑡𝐴)
1451443adant2 1100 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → 𝑡𝐴)
146145adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑡𝐴)
1471463ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡𝐴)
14874ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝐹𝑡) = (𝐹𝑤))
1491483adant3 1101 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑡) = (𝐹𝑤))
150 fniniseg 6378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 Fn 𝐴 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
151121, 3, 1503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
152138, 151mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢))
153152simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑤) = 𝑢)
1541533adant1r 1359 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑤) = 𝑢)
155149, 154eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑡) = 𝑢)
156147, 155jca 553 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢))
157 fniniseg 6378 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 Fn 𝐴 → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1583, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1591583ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
160159ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1611603adant3 1101 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
162156, 161mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ (𝐹 “ {𝑢}))
163 rspa 2959 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤𝑡 ∈ (𝐹 “ {𝑢})) → ¬ 𝑡𝑅𝑤)
164143, 162, 163syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ¬ 𝑡𝑅𝑤)
1651643exp 1283 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝑢 ∈ ran 𝐹 → (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤)))
166117, 118, 165rexlimd 3055 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤))
16771, 166mpd 15 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑤)
168107, 167chvarv 2299 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎)
16999, 168chvarv 2299 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎)
17091, 169chvarv 2299 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡)
17183, 170chvarv 2299 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤)) → ¬ 𝑤𝑅𝑡)
17264, 65, 72, 75, 171syl31anc 1369 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑤𝑅𝑡)
173172, 167jca 553 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤))
174 weso 5134 . . . . . . . . . . . . . . . 16 (𝑅 We 𝐴𝑅 Or 𝐴)
1758, 174syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑅 Or 𝐴)
176175adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑅 Or 𝐴)
1771763ad2antl1 1243 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑅 Or 𝐴)
17843sselda 3636 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ran 𝐺) → 𝑤𝐴)
1791783adant3 1101 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → 𝑤𝐴)
180179adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤𝐴)
181 sotrieq2 5092 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴 ∧ (𝑤𝐴𝑡𝐴)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
182177, 180, 146, 181syl12anc 1364 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
183173, 182mpbird 247 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤 = 𝑡)
18455, 63, 183syl2anc 694 . . . . . . . . . 10 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → 𝑤 = 𝑡)
185184ex 449 . . . . . . . . 9 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
18652, 53, 54, 185syl3anc 1366 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
187186ralrimivva 3000 . . . . . . 7 (𝜑 → ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
18851, 187jca 553 . . . . . 6 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
189 dff13 6552 . . . . . 6 ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
190188, 189sylibr 224 . . . . 5 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹)
191 riotaex 6655 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
192191rgenw 2953 . . . . . . . . . . . . 13 𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
193192a1i 11 . . . . . . . . . . . 12 (𝜑 → ∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
19441fnmpt 6058 . . . . . . . . . . . 12 (∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V → 𝐺 Fn ran 𝐹)
195193, 194syl 17 . . . . . . . . . . 11 (𝜑𝐺 Fn ran 𝐹)
196 dffn3 6092 . . . . . . . . . . . 12 (𝐺 Fn ran 𝐹𝐺:ran 𝐹⟶ran 𝐺)
197196biimpi 206 . . . . . . . . . . 11 (𝐺 Fn ran 𝐹𝐺:ran 𝐹⟶ran 𝐺)
198195, 197syl 17 . . . . . . . . . 10 (𝜑𝐺:ran 𝐹⟶ran 𝐺)
199198ffvelrnda 6399 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) ∈ ran 𝐺)
200 fvres 6245 . . . . . . . . . . 11 ((𝐺𝑢) ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)) = (𝐹‘(𝐺𝑢)))
201199, 200syl 17 . . . . . . . . . 10 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)) = (𝐹‘(𝐺𝑢)))
20217, 15sylibr 224 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹)
203191a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
20441fvmpt2 6330 . . . . . . . . . . . . . 14 ((𝑢 ∈ ran 𝐹 ∧ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V) → (𝐺𝑢) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
205202, 203, 204syl2anc 694 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
206205, 21eqeltrd 2730 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) ∈ (𝐹 “ {𝑢}))
207 fvex 6239 . . . . . . . . . . . . . 14 (𝐺𝑢) ∈ V
208 eleq1 2718 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐺𝑢) → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝐺𝑢) ∈ (𝐹 “ {𝑢})))
209 eleq1 2718 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐺𝑢) → (𝑤𝐴 ↔ (𝐺𝑢) ∈ 𝐴))
210 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐺𝑢) → (𝐹𝑤) = (𝐹‘(𝐺𝑢)))
211210eqeq1d 2653 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐺𝑢) → ((𝐹𝑤) = 𝑢 ↔ (𝐹‘(𝐺𝑢)) = 𝑢))
212209, 211anbi12d 747 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐺𝑢) → ((𝑤𝐴 ∧ (𝐹𝑤) = 𝑢) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
213208, 212bibi12d 334 . . . . . . . . . . . . . . 15 (𝑤 = (𝐺𝑢) → ((𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)) ↔ ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢))))
214213imbi2d 329 . . . . . . . . . . . . . 14 (𝑤 = (𝐺𝑢) → ((𝜑 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢))) ↔ (𝜑 → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))))
2153, 150syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
216207, 214, 215vtocl 3290 . . . . . . . . . . . . 13 (𝜑 → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
217216adantr 480 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
218206, 217mpbid 222 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢))
219218simprd 478 . . . . . . . . . 10 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹‘(𝐺𝑢)) = 𝑢)
220201, 219eqtr2d 2686 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)))
221 fveq2 6229 . . . . . . . . . . 11 (𝑤 = (𝐺𝑢) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)))
222221eqeq2d 2661 . . . . . . . . . 10 (𝑤 = (𝐺𝑢) → (𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤) ↔ 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢))))
223222rspcev 3340 . . . . . . . . 9 (((𝐺𝑢) ∈ ran 𝐺𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢))) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
224199, 220, 223syl2anc 694 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
225224ralrimiva 2995 . . . . . . 7 (𝜑 → ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
22651, 225jca 553 . . . . . 6 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
227 dffo3 6414 . . . . . 6 ((𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
228226, 227sylibr 224 . . . . 5 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹)
229190, 228jca 553 . . . 4 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹))
230 df-f1o 5933 . . . 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 2793 . . . . . 6 𝑣𝐹
233 nfcv 2793 . . . . . . . . 9 𝑣ran 𝐹
234 nfriota1 6658 . . . . . . . . 9 𝑣(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
235233, 234nfmpt 4779 . . . . . . . 8 𝑣(𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
23641, 235nfcxfr 2791 . . . . . . 7 𝑣𝐺
237236nfrn 5400 . . . . . 6 𝑣ran 𝐺
238232, 237nfres 5430 . . . . 5 𝑣(𝐹 ↾ ran 𝐺)
239238, 237, 233nff1o 6173 . . . 4 𝑣(𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹
240 reseq2 5423 . . . . 5 (𝑣 = ran 𝐺 → (𝐹𝑣) = (𝐹 ↾ ran 𝐺))
241 id 22 . . . . 5 (𝑣 = ran 𝐺𝑣 = ran 𝐺)
242 eqidd 2652 . . . . 5 (𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹)
243240, 241, 242f1oeq123d 6171 . . . 4 (𝑣 = ran 𝐺 → ((𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹))
244239, 243rspce 3335 . . 3 ((ran 𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹) → ∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹)
24547, 231, 244syl2anc 694 . 2 (𝜑 → ∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹)
246 reseq2 5423 . . . 4 (𝑣 = 𝑥 → (𝐹𝑣) = (𝐹𝑥))
247 id 22 . . . 4 (𝑣 = 𝑥𝑣 = 𝑥)
248 eqidd 2652 . . . 4 (𝑣 = 𝑥 → ran 𝐹 = ran 𝐹)
249246, 247, 248f1oeq123d 6171 . . 3 (𝑣 = 𝑥 → ((𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ (𝐹𝑥):𝑥1-1-onto→ran 𝐹))
250249cbvrexv 3202 . 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 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  ∃!wreu 2943  Vcvv 3231  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   class class class wbr 4685  cmpt 4762   Or wor 5063   We wwe 5101  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146   Fn wfn 5921  wf 5922  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926  crio 6650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651
This theorem is referenced by:  wessf1orn  39686
  Copyright terms: Public domain W3C validator