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 39860
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 5695 . . . . . . . . 9 (𝐹 “ {𝑢}) ⊆ dom 𝐹
21a1i 11 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ⊆ dom 𝐹)
3 wessf1ornlem.f . . . . . . . . . 10 (𝜑𝐹 Fn 𝐴)
4 fndm 6201 . . . . . . . . . 10 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
53, 4syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
65adantr 468 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → dom 𝐹 = 𝐴)
72, 6sseqtrd 3838 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ⊆ 𝐴)
8 wessf1ornlem.r . . . . . . . . . 10 (𝜑𝑅 We 𝐴)
98adantr 468 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → 𝑅 We 𝐴)
101, 5syl5sseq 3850 . . . . . . . . . . 11 (𝜑 → (𝐹 “ {𝑢}) ⊆ 𝐴)
11 wessf1ornlem.a . . . . . . . . . . 11 (𝜑𝐴𝑉)
12 ssexg 4999 . . . . . . . . . . 11 (((𝐹 “ {𝑢}) ⊆ 𝐴𝐴𝑉) → (𝐹 “ {𝑢}) ∈ V)
1310, 11, 12syl2anc 575 . . . . . . . . . 10 (𝜑 → (𝐹 “ {𝑢}) ∈ V)
1413adantr 468 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ∈ V)
15 inisegn0 5707 . . . . . . . . . . 11 (𝑢 ∈ ran 𝐹 ↔ (𝐹 “ {𝑢}) ≠ ∅)
1615biimpi 207 . . . . . . . . . 10 (𝑢 ∈ ran 𝐹 → (𝐹 “ {𝑢}) ≠ ∅)
1716adantl 469 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹 “ {𝑢}) ≠ ∅)
18 wereu 5307 . . . . . . . . 9 ((𝑅 We 𝐴 ∧ ((𝐹 “ {𝑢}) ∈ V ∧ (𝐹 “ {𝑢}) ⊆ 𝐴 ∧ (𝐹 “ {𝑢}) ≠ ∅)) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
199, 14, 7, 17, 18syl13anc 1484 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
20 riotacl 6849 . . . . . . . 8 (∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (𝐹 “ {𝑢}))
2119, 20syl 17 . . . . . . 7 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (𝐹 “ {𝑢}))
227, 21sseldd 3799 . . . . . 6 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
2322ralrimiva 3154 . . . . 5 (𝜑 → ∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴)
24 wessf1ornlem.g . . . . . . 7 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))
25 sneq 4380 . . . . . . . . . . 11 (𝑦 = 𝑢 → {𝑦} = {𝑢})
2625imaeq2d 5676 . . . . . . . . . 10 (𝑦 = 𝑢 → (𝐹 “ {𝑦}) = (𝐹 “ {𝑢}))
2726raleqdv 3333 . . . . . . . . . 10 (𝑦 = 𝑢 → (∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
2826, 27riotaeqbidv 6838 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥))
29 breq1 4847 . . . . . . . . . . . . . . 15 (𝑧 = 𝑡 → (𝑧𝑅𝑥𝑡𝑅𝑥))
3029notbid 309 . . . . . . . . . . . . . 14 (𝑧 = 𝑡 → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑡𝑅𝑥))
3130cbvralv 3360 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥)
3231a1i 11 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥))
33 breq2 4848 . . . . . . . . . . . . . 14 (𝑥 = 𝑣 → (𝑡𝑅𝑥𝑡𝑅𝑣))
3433notbid 309 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (¬ 𝑡𝑅𝑥 ↔ ¬ 𝑡𝑅𝑣))
3534ralbidv 3174 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3632, 35bitrd 270 . . . . . . . . . . 11 (𝑥 = 𝑣 → (∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3736cbvriotav 6846 . . . . . . . . . 10 (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
3837a1i 11 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑢})∀𝑧 ∈ (𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
3928, 38eqtrd 2840 . . . . . . . 8 (𝑦 = 𝑢 → (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4039cbvmptv 4944 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↦ (𝑥 ∈ (𝐹 “ {𝑦})∀𝑧 ∈ (𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) = (𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4124, 40eqtri 2828 . . . . . 6 𝐺 = (𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
4241rnmptss 6614 . . . . 5 (∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴 → ran 𝐺𝐴)
4323, 42syl 17 . . . 4 (𝜑 → ran 𝐺𝐴)
4411, 43ssexd 5000 . . . . 5 (𝜑 → ran 𝐺 ∈ V)
45 elpwg 4359 . . . . 5 (ran 𝐺 ∈ V → (ran 𝐺 ∈ 𝒫 𝐴 ↔ ran 𝐺𝐴))
4644, 45syl 17 . . . 4 (𝜑 → (ran 𝐺 ∈ 𝒫 𝐴 ↔ ran 𝐺𝐴))
4743, 46mpbird 248 . . 3 (𝜑 → ran 𝐺 ∈ 𝒫 𝐴)
48 dffn3 6267 . . . . . . . . . 10 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
4948biimpi 207 . . . . . . . . 9 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
503, 49syl 17 . . . . . . . 8 (𝜑𝐹:𝐴⟶ran 𝐹)
5150, 43fssresd 6286 . . . . . . 7 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹)
52 simpl 470 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝜑)
53 simprl 778 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝑤 ∈ ran 𝐺)
54 simprr 780 . . . . . . . . 9 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → 𝑡 ∈ ran 𝐺)
55 simpl 470 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺))
56 fvres 6427 . . . . . . . . . . . . . . 15 (𝑤 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑤) = (𝐹𝑤))
5756eqcomd 2812 . . . . . . . . . . . . . 14 (𝑤 ∈ ran 𝐺 → (𝐹𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
5857ad2antrr 708 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤))
59 simpr 473 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡))
60 fvres 6427 . . . . . . . . . . . . . 14 (𝑡 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹𝑡))
6160ad2antlr 709 . . . . . . . . . . . . 13 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹𝑡))
6258, 59, 613eqtrd 2844 . . . . . . . . . . . 12 (((𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = (𝐹𝑡))
63623adantl1 1200 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹𝑤) = (𝐹𝑡))
64 simpl1 1235 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝜑)
65 simpl3 1239 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑡 ∈ ran 𝐺)
66 vex 3394 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ V
6741elrnmpt 5573 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ V → (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
6968biimpi 207 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ran 𝐺 → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
7069adantr 468 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ran 𝐺 ∧ (𝐹𝑤) = (𝐹𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
71703ad2antl2 1230 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
7271, 68sylibr 225 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤 ∈ ran 𝐺)
73 id 22 . . . . . . . . . . . . . . . 16 ((𝐹𝑤) = (𝐹𝑡) → (𝐹𝑤) = (𝐹𝑡))
7473eqcomd 2812 . . . . . . . . . . . . . . 15 ((𝐹𝑤) = (𝐹𝑡) → (𝐹𝑡) = (𝐹𝑤))
7574adantl 469 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝐹𝑡) = (𝐹𝑤))
76 eleq1w 2868 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → (𝑏 ∈ ran 𝐺𝑤 ∈ ran 𝐺))
77763anbi3d 1559 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → ((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ↔ (𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺)))
78 fveq2 6408 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑤 → (𝐹𝑏) = (𝐹𝑤))
7978eqeq2d 2816 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → ((𝐹𝑡) = (𝐹𝑏) ↔ (𝐹𝑡) = (𝐹𝑤)))
8077, 79anbi12d 618 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) ↔ ((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤))))
81 breq1 4847 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑤 → (𝑏𝑅𝑡𝑤𝑅𝑡))
8281notbid 309 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (¬ 𝑏𝑅𝑡 ↔ ¬ 𝑤𝑅𝑡))
8380, 82imbi12d 335 . . . . . . . . . . . . . . 15 (𝑏 = 𝑤 → ((((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡) ↔ (((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤)) → ¬ 𝑤𝑅𝑡)))
84 eleq1w 2868 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑡 → (𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺))
85843anbi2d 1558 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → ((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ↔ (𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺)))
86 fveqeq2 6417 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → ((𝐹𝑎) = (𝐹𝑏) ↔ (𝐹𝑡) = (𝐹𝑏)))
8785, 86anbi12d 618 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑡 → (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) ↔ ((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏))))
88 breq2 4848 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑡 → (𝑏𝑅𝑎𝑏𝑅𝑡))
8988notbid 309 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑡 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑏𝑅𝑡))
9087, 89imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑡 → ((((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎) ↔ (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡)))
91 eleq1w 2868 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺))
92913anbi3d 1559 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ↔ (𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺)))
93 fveq2 6408 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝐹𝑡) = (𝐹𝑏))
9493eqeq2d 2816 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝐹𝑎) = (𝐹𝑡) ↔ (𝐹𝑎) = (𝐹𝑏)))
9592, 94anbi12d 618 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) ↔ ((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏))))
96 breq1 4847 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → (𝑡𝑅𝑎𝑏𝑅𝑎))
9796notbid 309 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → (¬ 𝑡𝑅𝑎 ↔ ¬ 𝑏𝑅𝑎))
9895, 97imbi12d 335 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑏 → ((((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎) ↔ (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎)))
99 eleq1w 2868 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑎 → (𝑤 ∈ ran 𝐺𝑎 ∈ ran 𝐺))
100993anbi2d 1558 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ↔ (𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺)))
101 fveqeq2 6417 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → ((𝐹𝑤) = (𝐹𝑡) ↔ (𝐹𝑎) = (𝐹𝑡)))
102100, 101anbi12d 618 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑎 → (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ↔ ((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡))))
103 breq2 4848 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → (𝑡𝑅𝑤𝑡𝑅𝑎))
104103notbid 309 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑎 → (¬ 𝑡𝑅𝑤 ↔ ¬ 𝑡𝑅𝑎))
105102, 104imbi12d 335 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑎 → ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑤) ↔ (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎)))
106 nfv 2005 . . . . . . . . . . . . . . . . . . . . . 22 𝑢𝜑
107 nfcv 2948 . . . . . . . . . . . . . . . . . . . . . . 23 𝑢𝑤
108 nfmpt1 4941 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑢(𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
10941, 108nfcxfr 2946 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑢𝐺
110109nfrn 5569 . . . . . . . . . . . . . . . . . . . . . . 23 𝑢ran 𝐺
111107, 110nfel 2961 . . . . . . . . . . . . . . . . . . . . . 22 𝑢 𝑤 ∈ ran 𝐺
112110nfcri 2942 . . . . . . . . . . . . . . . . . . . . . 22 𝑢 𝑡 ∈ ran 𝐺
113106, 111, 112nf3an 1993 . . . . . . . . . . . . . . . . . . . . 21 𝑢(𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)
114 nfv 2005 . . . . . . . . . . . . . . . . . . . . 21 𝑢(𝐹𝑤) = (𝐹𝑡)
115113, 114nfan 1990 . . . . . . . . . . . . . . . . . . . 20 𝑢((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡))
116 nfv 2005 . . . . . . . . . . . . . . . . . . . 20 𝑢 ¬ 𝑡𝑅𝑤
117 simp3 1161 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
118117eqcomd 2812 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)
119 simp11 1253 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝜑)
120 simp2 1160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑢 ∈ ran 𝐹)
121 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
122 breq2 4848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = 𝑤 → (𝑡𝑅𝑣𝑡𝑅𝑤))
123122notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = 𝑤 → (¬ 𝑡𝑅𝑣 ↔ ¬ 𝑡𝑅𝑤))
124123ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 = 𝑤 → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
125124cbvriotav 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
126125a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
127121, 126eqtr2d 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
1281273ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)
129124cbvreuv 3362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
13019, 129sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ ran 𝐹) → ∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
131 riota1 6853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃!𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
132130, 131syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ ran 𝐹) → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
1331323adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (𝑤 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤))
134128, 133mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤))
135134simpld 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (𝐹 “ {𝑢}))
136119, 120, 117, 135syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (𝐹 “ {𝑢}))
137119, 120, 19syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
138124riota2 6857 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑤 ∈ (𝐹 “ {𝑢}) ∧ ∃!𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
139136, 137, 138syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤))
140118, 139mpbird 248 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
1411403adant1r 1216 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)
14243sselda 3798 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑡 ∈ ran 𝐺) → 𝑡𝐴)
1431423adant2 1154 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → 𝑡𝐴)
144143adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑡𝐴)
1451443ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡𝐴)
14674ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝐹𝑡) = (𝐹𝑤))
1471463adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑡) = (𝐹𝑤))
148 fniniseg 6560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 Fn 𝐴 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
149119, 3, 1483syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
150136, 149mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢))
151150simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑤) = 𝑢)
1521513adant1r 1216 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑤) = 𝑢)
153147, 152eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹𝑡) = 𝑢)
154145, 153jca 503 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢))
155 fniniseg 6560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 Fn 𝐴 → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1563, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1571563ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
158157ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
1591583adant3 1155 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡 ∈ (𝐹 “ {𝑢}) ↔ (𝑡𝐴 ∧ (𝐹𝑡) = 𝑢)))
160154, 159mpbird 248 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ (𝐹 “ {𝑢}))
161 rspa 3118 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤𝑡 ∈ (𝐹 “ {𝑢})) → ¬ 𝑡𝑅𝑤)
162141, 160, 161syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) ∧ 𝑢 ∈ ran 𝐹𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ¬ 𝑡𝑅𝑤)
1631623exp 1141 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝑢 ∈ ran 𝐹 → (𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤)))
164115, 116, 163rexlimd 3214 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (∃𝑢 ∈ ran 𝐹 𝑤 = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤))
16571, 164mpd 15 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑤)
166105, 165chvarv 2437 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑡)) → ¬ 𝑡𝑅𝑎)
16798, 166chvarv 2437 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑎) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑎)
16890, 167chvarv 2437 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ ran 𝐺𝑏 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑏)) → ¬ 𝑏𝑅𝑡)
16983, 168chvarv 2437 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ran 𝐺𝑤 ∈ ran 𝐺) ∧ (𝐹𝑡) = (𝐹𝑤)) → ¬ 𝑤𝑅𝑡)
17064, 65, 72, 75, 169syl31anc 1485 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → ¬ 𝑤𝑅𝑡)
171170, 165jca 503 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤))
172 weso 5302 . . . . . . . . . . . . . . . 16 (𝑅 We 𝐴𝑅 Or 𝐴)
1738, 172syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑅 Or 𝐴)
174173adantr 468 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑅 Or 𝐴)
1751743ad2antl1 1229 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑅 Or 𝐴)
17643sselda 3798 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ran 𝐺) → 𝑤𝐴)
1771763adant3 1155 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → 𝑤𝐴)
178177adantr 468 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤𝐴)
179 sotrieq2 5260 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴 ∧ (𝑤𝐴𝑡𝐴)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
180175, 178, 144, 179syl12anc 856 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)))
181171, 180mpbird 248 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ (𝐹𝑤) = (𝐹𝑡)) → 𝑤 = 𝑡)
18255, 63, 181syl2anc 575 . . . . . . . . . 10 (((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → 𝑤 = 𝑡)
183182ex 399 . . . . . . . . 9 ((𝜑𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
18452, 53, 54, 183syl3anc 1483 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺)) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
185184ralrimivva 3159 . . . . . . 7 (𝜑 → ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))
18651, 185jca 503 . . . . . 6 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
187 dff13 6736 . . . . . 6 ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)))
188186, 187sylibr 225 . . . . 5 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹)
189 riotaex 6839 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
190189rgenw 3112 . . . . . . . . . . . . 13 𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V
191190a1i 11 . . . . . . . . . . . 12 (𝜑 → ∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
19241fnmpt 6231 . . . . . . . . . . . 12 (∀𝑢 ∈ ran 𝐹(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V → 𝐺 Fn ran 𝐹)
193191, 192syl 17 . . . . . . . . . . 11 (𝜑𝐺 Fn ran 𝐹)
194 dffn3 6267 . . . . . . . . . . . 12 (𝐺 Fn ran 𝐹𝐺:ran 𝐹⟶ran 𝐺)
195194biimpi 207 . . . . . . . . . . 11 (𝐺 Fn ran 𝐹𝐺:ran 𝐹⟶ran 𝐺)
196193, 195syl 17 . . . . . . . . . 10 (𝜑𝐺:ran 𝐹⟶ran 𝐺)
197196ffvelrnda 6581 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) ∈ ran 𝐺)
198 fvres 6427 . . . . . . . . . . 11 ((𝐺𝑢) ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)) = (𝐹‘(𝐺𝑢)))
199197, 198syl 17 . . . . . . . . . 10 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)) = (𝐹‘(𝐺𝑢)))
20017, 15sylibr 225 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹)
201189a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ ran 𝐹) → (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V)
20241fvmpt2 6512 . . . . . . . . . . . . . 14 ((𝑢 ∈ ran 𝐹 ∧ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V) → (𝐺𝑢) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
203200, 201, 202syl2anc 575 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) = (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
204203, 21eqeltrd 2885 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ ran 𝐹) → (𝐺𝑢) ∈ (𝐹 “ {𝑢}))
205 fvex 6421 . . . . . . . . . . . . . 14 (𝐺𝑢) ∈ V
206 eleq1 2873 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐺𝑢) → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝐺𝑢) ∈ (𝐹 “ {𝑢})))
207 eleq1 2873 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐺𝑢) → (𝑤𝐴 ↔ (𝐺𝑢) ∈ 𝐴))
208 fveqeq2 6417 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐺𝑢) → ((𝐹𝑤) = 𝑢 ↔ (𝐹‘(𝐺𝑢)) = 𝑢))
209207, 208anbi12d 618 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐺𝑢) → ((𝑤𝐴 ∧ (𝐹𝑤) = 𝑢) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
210206, 209bibi12d 336 . . . . . . . . . . . . . . 15 (𝑤 = (𝐺𝑢) → ((𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)) ↔ ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢))))
211210imbi2d 331 . . . . . . . . . . . . . 14 (𝑤 = (𝐺𝑢) → ((𝜑 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢))) ↔ (𝜑 → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))))
2123, 148syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ (𝐹 “ {𝑢}) ↔ (𝑤𝐴 ∧ (𝐹𝑤) = 𝑢)))
213205, 211, 212vtocl 3452 . . . . . . . . . . . . 13 (𝜑 → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
214213adantr 468 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐺𝑢) ∈ (𝐹 “ {𝑢}) ↔ ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢)))
215204, 214mpbid 223 . . . . . . . . . . 11 ((𝜑𝑢 ∈ ran 𝐹) → ((𝐺𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑢)) = 𝑢))
216215simprd 485 . . . . . . . . . 10 ((𝜑𝑢 ∈ ran 𝐹) → (𝐹‘(𝐺𝑢)) = 𝑢)
217199, 216eqtr2d 2841 . . . . . . . . 9 ((𝜑𝑢 ∈ ran 𝐹) → 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)))
218 fveq2 6408 . . . . . . . . . 10 (𝑤 = (𝐺𝑢) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢)))
219218rspceeqv 3520 . . . . . . . . 9 (((𝐺𝑢) ∈ ran 𝐺𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺𝑢))) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
220197, 217, 219syl2anc 575 . . . . . . . 8 ((𝜑𝑢 ∈ ran 𝐹) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
221220ralrimiva 3154 . . . . . . 7 (𝜑 → ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))
22251, 221jca 503 . . . . . 6 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
223 dffo3 6596 . . . . . 6 ((𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)))
224222, 223sylibr 225 . . . . 5 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹)
225188, 224jca 503 . . . 4 (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹))
226 df-f1o 6108 . . . 4 ((𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺onto→ran 𝐹))
227225, 226sylibr 225 . . 3 (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹)
228 nfcv 2948 . . . . . 6 𝑣𝐹
229 nfcv 2948 . . . . . . . . 9 𝑣ran 𝐹
230 nfriota1 6842 . . . . . . . . 9 𝑣(𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)
231229, 230nfmpt 4940 . . . . . . . 8 𝑣(𝑢 ∈ ran 𝐹 ↦ (𝑣 ∈ (𝐹 “ {𝑢})∀𝑡 ∈ (𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))
23241, 231nfcxfr 2946 . . . . . . 7 𝑣𝐺
233232nfrn 5569 . . . . . 6 𝑣ran 𝐺
234228, 233nfres 5599 . . . . 5 𝑣(𝐹 ↾ ran 𝐺)
235234, 233, 229nff1o 6351 . . . 4 𝑣(𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹
236 reseq2 5592 . . . . 5 (𝑣 = ran 𝐺 → (𝐹𝑣) = (𝐹 ↾ ran 𝐺))
237 id 22 . . . . 5 (𝑣 = ran 𝐺𝑣 = ran 𝐺)
238 eqidd 2807 . . . . 5 (𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹)
239236, 237, 238f1oeq123d 6349 . . . 4 (𝑣 = ran 𝐺 → ((𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹))
240235, 239rspce 3497 . . 3 ((ran 𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺1-1-onto→ran 𝐹) → ∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹)
24147, 227, 240syl2anc 575 . 2 (𝜑 → ∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹)
242 reseq2 5592 . . . 4 (𝑣 = 𝑥 → (𝐹𝑣) = (𝐹𝑥))
243 id 22 . . . 4 (𝑣 = 𝑥𝑣 = 𝑥)
244 eqidd 2807 . . . 4 (𝑣 = 𝑥 → ran 𝐹 = ran 𝐹)
245242, 243, 244f1oeq123d 6349 . . 3 (𝑣 = 𝑥 → ((𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ (𝐹𝑥):𝑥1-1-onto→ran 𝐹))
246245cbvrexv 3361 . 2 (∃𝑣 ∈ 𝒫 𝐴(𝐹𝑣):𝑣1-1-onto→ran 𝐹 ↔ ∃𝑥 ∈ 𝒫 𝐴(𝐹𝑥):𝑥1-1-onto→ran 𝐹)
247241, 246sylib 209 1 (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹𝑥):𝑥1-1-onto→ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2978  wral 3096  wrex 3097  ∃!wreu 3098  Vcvv 3391  wss 3769  c0 4116  𝒫 cpw 4351  {csn 4370   class class class wbr 4844  cmpt 4923   Or wor 5231   We wwe 5269  ccnv 5310  dom cdm 5311  ran crn 5312  cres 5313  cima 5314   Fn wfn 6096  wf 6097  1-1wf1 6098  ontowfo 6099  1-1-ontowf1o 6100  cfv 6101  crio 6834
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835
This theorem is referenced by:  wessf1orn  39861
  Copyright terms: Public domain W3C validator