Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poseq Structured version   Visualization version   GIF version

Theorem poseq 32079
Description: A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.)
Hypotheses
Ref Expression
poseq.1 𝑅 Po (𝐴 ∪ {∅})
poseq.2 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴}
poseq.3 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
Assertion
Ref Expression
poseq 𝑆 Po 𝐹
Distinct variable groups:   𝐴,𝑓,𝑥   𝑓,𝑔,𝑦,𝑥   𝑓,𝐹,𝑔,𝑥   𝑅,𝑓,𝑔,𝑥
Allowed substitution hints:   𝐴(𝑦,𝑔)   𝑅(𝑦)   𝑆(𝑥,𝑦,𝑓,𝑔)   𝐹(𝑦)

Proof of Theorem poseq
Dummy variables 𝑏 𝑎 𝑐 𝑡 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poseq.1 . . . . . . . . . . . 12 𝑅 Po (𝐴 ∪ {∅})
2 poseq.2 . . . . . . . . . . . . . 14 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴}
3 feq2 6241 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑏 → (𝑓:𝑥𝐴𝑓:𝑏𝐴))
43cbvrexv 3368 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏𝐴)
54abbii 2930 . . . . . . . . . . . . . 14 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
62, 5eqtri 2835 . . . . . . . . . . . . 13 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
76orderseqlem 32078 . . . . . . . . . . . 12 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
8 poirr 5250 . . . . . . . . . . . 12 ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
91, 7, 8sylancr 577 . . . . . . . . . . 11 (𝑎𝐹 → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
109intnand 478 . . . . . . . . . 10 (𝑎𝐹 → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1110adantr 468 . . . . . . . . 9 ((𝑎𝐹𝑥 ∈ On) → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1211nrexdv 3195 . . . . . . . 8 (𝑎𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1312adantr 468 . . . . . . 7 ((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
14 imnan 388 . . . . . . 7 (((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))) ↔ ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
1513, 14mpbi 221 . . . . . 6 ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
16 vex 3401 . . . . . . 7 𝑎 ∈ V
17 eleq1w 2875 . . . . . . . . 9 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
1817anbi1d 617 . . . . . . . 8 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
19 fveq1 6410 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
2019eqeq1d 2815 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
2120ralbidv 3181 . . . . . . . . . 10 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
22 fveq1 6410 . . . . . . . . . . 11 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
2322breq1d 4861 . . . . . . . . . 10 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
2421, 23anbi12d 618 . . . . . . . . 9 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2524rexbidv 3247 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2618, 25anbi12d 618 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
27 eleq1w 2875 . . . . . . . . 9 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
2827anbi2d 616 . . . . . . . 8 (𝑔 = 𝑎 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑎𝐹)))
29 fveq1 6410 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
3029eqeq2d 2823 . . . . . . . . . . 11 (𝑔 = 𝑎 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑎𝑦)))
3130ralbidv 3181 . . . . . . . . . 10 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦)))
32 fveq1 6410 . . . . . . . . . . 11 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
3332breq2d 4863 . . . . . . . . . 10 (𝑔 = 𝑎 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑎𝑥)))
3431, 33anbi12d 618 . . . . . . . . 9 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3534rexbidv 3247 . . . . . . . 8 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3628, 35anbi12d 618 . . . . . . 7 (𝑔 = 𝑎 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))))
37 poseq.3 . . . . . . 7 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
3816, 16, 26, 36, 37brab 5200 . . . . . 6 (𝑎𝑆𝑎 ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3915, 38mtbir 314 . . . . 5 ¬ 𝑎𝑆𝑎
40 vex 3401 . . . . . . . 8 𝑏 ∈ V
41 raleq 3334 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦)))
42 fveq2 6411 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓𝑥) = (𝑓𝑧))
43 fveq2 6411 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑔𝑥) = (𝑔𝑧))
4442, 43breq12d 4864 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑧)𝑅(𝑔𝑧)))
4541, 44anbi12d 618 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧))))
4645cbvrexv 3368 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)))
4720ralbidv 3181 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦)))
48 fveq1 6410 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (𝑓𝑧) = (𝑎𝑧))
4948breq1d 4861 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((𝑓𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑔𝑧)))
5047, 49anbi12d 618 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5150rexbidv 3247 . . . . . . . . . 10 (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5246, 51syl5bb 274 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5318, 52anbi12d 618 . . . . . . . 8 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)))))
54 eleq1w 2875 . . . . . . . . . 10 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
5554anbi2d 616 . . . . . . . . 9 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
56 fveq1 6410 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
5756eqeq2d 2823 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
5857ralbidv 3181 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦)))
59 fveq1 6410 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝑧) = (𝑏𝑧))
6059breq2d 4863 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑏𝑧)))
6158, 60anbi12d 618 . . . . . . . . . 10 (𝑔 = 𝑏 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6261rexbidv 3247 . . . . . . . . 9 (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6355, 62anbi12d 618 . . . . . . . 8 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)))))
6416, 40, 53, 63, 37brab 5200 . . . . . . 7 (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
65 vex 3401 . . . . . . . 8 𝑐 ∈ V
66 eleq1w 2875 . . . . . . . . . 10 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
6766anbi1d 617 . . . . . . . . 9 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
68 raleq 3334 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦)))
69 fveq2 6411 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑓𝑥) = (𝑓𝑤))
70 fveq2 6411 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑔𝑥) = (𝑔𝑤))
7169, 70breq12d 4864 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑤)𝑅(𝑔𝑤)))
7268, 71anbi12d 618 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤))))
7372cbvrexv 3368 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)))
74 fveq1 6410 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
7574eqeq1d 2815 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
7675ralbidv 3181 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦)))
77 fveq1 6410 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝑤) = (𝑏𝑤))
7877breq1d 4861 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑔𝑤)))
7976, 78anbi12d 618 . . . . . . . . . . 11 (𝑓 = 𝑏 → ((∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8079rexbidv 3247 . . . . . . . . . 10 (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8173, 80syl5bb 274 . . . . . . . . 9 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8267, 81anbi12d 618 . . . . . . . 8 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)))))
83 eleq1w 2875 . . . . . . . . . 10 (𝑔 = 𝑐 → (𝑔𝐹𝑐𝐹))
8483anbi2d 616 . . . . . . . . 9 (𝑔 = 𝑐 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑐𝐹)))
85 fveq1 6410 . . . . . . . . . . . . 13 (𝑔 = 𝑐 → (𝑔𝑦) = (𝑐𝑦))
8685eqeq2d 2823 . . . . . . . . . . . 12 (𝑔 = 𝑐 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑐𝑦)))
8786ralbidv 3181 . . . . . . . . . . 11 (𝑔 = 𝑐 → (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
88 fveq1 6410 . . . . . . . . . . . 12 (𝑔 = 𝑐 → (𝑔𝑤) = (𝑐𝑤))
8988breq2d 4863 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑏𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
9087, 89anbi12d 618 . . . . . . . . . 10 (𝑔 = 𝑐 → ((∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9190rexbidv 3247 . . . . . . . . 9 (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9284, 91anbi12d 618 . . . . . . . 8 (𝑔 = 𝑐 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))) ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
9340, 65, 82, 92, 37brab 5200 . . . . . . 7 (𝑏𝑆𝑐 ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
94 simplll 782 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑎𝐹)
95 simplrr 787 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑐𝐹)
96 an4 638 . . . . . . . . . . . . 13 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
97962rexbii 3237 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
98 reeanv 3302 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9997, 98bitri 266 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
100 eloni 5953 . . . . . . . . . . . . . 14 (𝑧 ∈ On → Ord 𝑧)
101 eloni 5953 . . . . . . . . . . . . . 14 (𝑤 ∈ On → Ord 𝑤)
102 ordtri3or 5975 . . . . . . . . . . . . . 14 ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
103100, 101, 102syl2an 585 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
104 simp1l 1247 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑧 ∈ On)
105 onelss 5985 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ On → (𝑧𝑤𝑧𝑤))
106105imp 395 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∈ On ∧ 𝑧𝑤) → 𝑧𝑤)
107106adantll 696 . . . . . . . . . . . . . . . . . . . 20 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → 𝑧𝑤)
108 ssralv 3870 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
109108anim2d 601 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦))))
110 r19.26 3259 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
111109, 110syl6ibr 243 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦))))
112 eqtr 2832 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → (𝑎𝑦) = (𝑐𝑦))
113112ralimi 3147 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
114111, 113syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
115107, 114syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
116115adantrd 481 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
1171163impia 1138 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
118 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑏𝑦) = (𝑏𝑧))
119 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑐𝑦) = (𝑐𝑧))
120118, 119eqeq12d 2828 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑏𝑦) = (𝑐𝑦) ↔ (𝑏𝑧) = (𝑐𝑧)))
121120rspcv 3505 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → (𝑏𝑧) = (𝑐𝑧)))
122 breq2 4855 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
123122biimpd 220 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧)))
124121, 123syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧))))
125124com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧))))
126125imp 395 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
127126ad2ant2lr 745 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
128127impcom 396 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
1291283adant1 1153 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
130 raleq 3334 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
131 fveq2 6411 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑎𝑡) = (𝑎𝑧))
132 fveq2 6411 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑐𝑡) = (𝑐𝑧))
133131, 132breq12d 4864 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
134130, 133anbi12d 618 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑧 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))))
135134rspcev 3509 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
136104, 117, 129, 135syl12anc 856 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
137136a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1381373exp 1141 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
1392orderseqlem 32078 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝐹 → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
140139ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
1412orderseqlem 32078 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝐹 → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
142141ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
1432orderseqlem 32078 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐𝐹 → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
144143ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
145140, 142, 1443jca 1151 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅})))
146 potr 5251 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
1471, 145, 146sylancr 577 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
148147impcom 396 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (𝑎𝑧)𝑅(𝑐𝑧))
149113, 148anim12i 602 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
150149anassrs 455 . . . . . . . . . . . . . . . . . 18 (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
151150, 135sylan2 582 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
152151exp32 409 . . . . . . . . . . . . . . . 16 (𝑧 ∈ On → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
153 raleq 3334 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
154153anbi2d 616 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
155110, 154syl5bb 274 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
156 fveq2 6411 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑏𝑧) = (𝑏𝑤))
157 fveq2 6411 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑐𝑧) = (𝑐𝑤))
158156, 157breq12d 4864 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((𝑏𝑧)𝑅(𝑐𝑧) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
159158anbi2d 616 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ↔ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
160155, 159anbi12d 618 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
161160imbi1d 332 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))) ↔ (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
162152, 161syl5ibcom 236 . . . . . . . . . . . . . . 15 (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
163162adantr 468 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
164 simp1r 1248 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑤 ∈ On)
165 onelss 5985 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ On → (𝑤𝑧𝑤𝑧))
166165imp 395 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ On ∧ 𝑤𝑧) → 𝑤𝑧)
167166adantlr 697 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → 𝑤𝑧)
168 ssralv 3870 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦)))
169168anim1d 600 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
170 r19.26 3259 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
171112ralimi 3147 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
172170, 171sylbir 226 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
173169, 172syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
174173adantrd 481 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
175167, 174syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
1761753impia 1138 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
177 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑎𝑦) = (𝑎𝑤))
178 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑏𝑦) = (𝑏𝑤))
179177, 178eqeq12d 2828 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑤 → ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑎𝑤) = (𝑏𝑤)))
180179rspcv 3505 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑤) = (𝑏𝑤)))
181 breq1 4854 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑤) = (𝑏𝑤) → ((𝑎𝑤)𝑅(𝑐𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
182181biimprd 239 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑤) = (𝑏𝑤) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤)))
183180, 182syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤))))
184183com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤))))
185184imp 395 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
186185ad2ant2rl 746 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
187186impcom 396 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
1881873adant1 1153 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
189 raleq 3334 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
190 fveq2 6411 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑎𝑡) = (𝑎𝑤))
191 fveq2 6411 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑐𝑡) = (𝑐𝑤))
192190, 191breq12d 4864 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑤)𝑅(𝑐𝑤)))
193189, 192anbi12d 618 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑤 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))))
194193rspcev 3509 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ On ∧ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
195164, 176, 188, 194syl12anc 856 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
196195a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1971963exp 1141 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
198138, 163, 1973jaod 1546 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧𝑤𝑧 = 𝑤𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
199103, 198mpd 15 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
200199rexlimivv 3231 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20199, 200sylbir 226 . . . . . . . . . 10 ((∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
202201impcom 396 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
20394, 95, 202jca31 506 . . . . . . . 8 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
204203an4s 642 . . . . . . 7 ((((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))) ∧ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20564, 93, 204syl2anb 587 . . . . . 6 ((𝑎𝑆𝑏𝑏𝑆𝑐) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
206 raleq 3334 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦)))
207 fveq2 6411 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑓𝑥) = (𝑓𝑡))
208 fveq2 6411 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
209207, 208breq12d 4864 . . . . . . . . . . 11 (𝑥 = 𝑡 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑡)𝑅(𝑔𝑡)))
210206, 209anbi12d 618 . . . . . . . . . 10 (𝑥 = 𝑡 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡))))
211210cbvrexv 3368 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)))
21220ralbidv 3181 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦)))
213 fveq1 6410 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑡) = (𝑎𝑡))
214213breq1d 4861 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑔𝑡)))
215212, 214anbi12d 618 . . . . . . . . . 10 (𝑓 = 𝑎 → ((∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
216215rexbidv 3247 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
217211, 216syl5bb 274 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
21818, 217anbi12d 618 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)))))
21983anbi2d 616 . . . . . . . 8 (𝑔 = 𝑐 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑐𝐹)))
22085eqeq2d 2823 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑐𝑦)))
221220ralbidv 3181 . . . . . . . . . 10 (𝑔 = 𝑐 → (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦)))
222 fveq1 6410 . . . . . . . . . . 11 (𝑔 = 𝑐 → (𝑔𝑡) = (𝑐𝑡))
223222breq2d 4863 . . . . . . . . . 10 (𝑔 = 𝑐 → ((𝑎𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑐𝑡)))
224221, 223anbi12d 618 . . . . . . . . 9 (𝑔 = 𝑐 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
225224rexbidv 3247 . . . . . . . 8 (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
226219, 225anbi12d 618 . . . . . . 7 (𝑔 = 𝑐 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))) ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
22716, 65, 218, 226, 37brab 5200 . . . . . 6 (𝑎𝑆𝑐 ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
228205, 227sylibr 225 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)
22939, 228pm3.2i 458 . . . 4 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230229a1i 11 . . 3 ((𝑎𝐹𝑏𝐹𝑐𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231230rgen3 3171 . 2 𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232 df-po 5239 . 2 (𝑆 Po 𝐹 ↔ ∀𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233231, 232mpbir 222 1 𝑆 Po 𝐹
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3o 1099  w3a 1100   = wceq 1637  wcel 2157  {cab 2799  wral 3103  wrex 3104  cun 3774  wss 3776  c0 4123  {csn 4377   class class class wbr 4851  {copab 4913   Po wpo 5237  Ord word 5942  Oncon0 5943  wf 6100  cfv 6104
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 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103
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 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-tr 4954  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-ord 5946  df-on 5947  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-fv 6112
This theorem is referenced by:  soseq  32080
  Copyright terms: Public domain W3C validator