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

Theorem poseq 33155
 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 6485 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑏 → (𝑓:𝑥𝐴𝑓:𝑏𝐴))
43cbvrexvw 3435 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏𝐴)
54abbii 2889 . . . . . . . . . . . . . 14 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
62, 5eqtri 2847 . . . . . . . . . . . . 13 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
76orderseqlem 33154 . . . . . . . . . . . 12 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
8 poirr 5472 . . . . . . . . . . . 12 ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
91, 7, 8sylancr 590 . . . . . . . . . . 11 (𝑎𝐹 → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
109intnand 492 . . . . . . . . . 10 (𝑎𝐹 → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1110adantr 484 . . . . . . . . 9 ((𝑎𝐹𝑥 ∈ On) → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1211nrexdv 3262 . . . . . . . 8 (𝑎𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1312adantr 484 . . . . . . 7 ((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
14 imnan 403 . . . . . . 7 (((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))) ↔ ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
1513, 14mpbi 233 . . . . . 6 ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
16 vex 3483 . . . . . . 7 𝑎 ∈ V
17 eleq1w 2898 . . . . . . . . 9 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
1817anbi1d 632 . . . . . . . 8 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
19 fveq1 6660 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
2019eqeq1d 2826 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
2120ralbidv 3192 . . . . . . . . . 10 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
22 fveq1 6660 . . . . . . . . . . 11 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
2322breq1d 5062 . . . . . . . . . 10 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
2421, 23anbi12d 633 . . . . . . . . 9 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2524rexbidv 3289 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2618, 25anbi12d 633 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
27 eleq1w 2898 . . . . . . . . 9 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
2827anbi2d 631 . . . . . . . 8 (𝑔 = 𝑎 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑎𝐹)))
29 fveq1 6660 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
3029eqeq2d 2835 . . . . . . . . . . 11 (𝑔 = 𝑎 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑎𝑦)))
3130ralbidv 3192 . . . . . . . . . 10 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦)))
32 fveq1 6660 . . . . . . . . . . 11 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
3332breq2d 5064 . . . . . . . . . 10 (𝑔 = 𝑎 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑎𝑥)))
3431, 33anbi12d 633 . . . . . . . . 9 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3534rexbidv 3289 . . . . . . . 8 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3628, 35anbi12d 633 . . . . . . 7 (𝑔 = 𝑎 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))))
37 poseq.3 . . . . . . 7 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
3816, 16, 26, 36, 37brab 5417 . . . . . 6 (𝑎𝑆𝑎 ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3915, 38mtbir 326 . . . . 5 ¬ 𝑎𝑆𝑎
40 vex 3483 . . . . . . . 8 𝑏 ∈ V
41 raleq 3396 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦)))
42 fveq2 6661 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓𝑥) = (𝑓𝑧))
43 fveq2 6661 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑔𝑥) = (𝑔𝑧))
4442, 43breq12d 5065 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑧)𝑅(𝑔𝑧)))
4541, 44anbi12d 633 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧))))
4645cbvrexvw 3435 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)))
4720ralbidv 3192 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦)))
48 fveq1 6660 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (𝑓𝑧) = (𝑎𝑧))
4948breq1d 5062 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((𝑓𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑔𝑧)))
5047, 49anbi12d 633 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5150rexbidv 3289 . . . . . . . . . 10 (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5246, 51syl5bb 286 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5318, 52anbi12d 633 . . . . . . . 8 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)))))
54 eleq1w 2898 . . . . . . . . . 10 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
5554anbi2d 631 . . . . . . . . 9 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
56 fveq1 6660 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
5756eqeq2d 2835 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
5857ralbidv 3192 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦)))
59 fveq1 6660 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝑧) = (𝑏𝑧))
6059breq2d 5064 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑏𝑧)))
6158, 60anbi12d 633 . . . . . . . . . 10 (𝑔 = 𝑏 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6261rexbidv 3289 . . . . . . . . 9 (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6355, 62anbi12d 633 . . . . . . . 8 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)))))
6416, 40, 53, 63, 37brab 5417 . . . . . . 7 (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
65 vex 3483 . . . . . . . 8 𝑐 ∈ V
66 eleq1w 2898 . . . . . . . . . 10 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
6766anbi1d 632 . . . . . . . . 9 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
68 raleq 3396 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦)))
69 fveq2 6661 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑓𝑥) = (𝑓𝑤))
70 fveq2 6661 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑔𝑥) = (𝑔𝑤))
7169, 70breq12d 5065 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑤)𝑅(𝑔𝑤)))
7268, 71anbi12d 633 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤))))
7372cbvrexvw 3435 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)))
74 fveq1 6660 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
7574eqeq1d 2826 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
7675ralbidv 3192 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦)))
77 fveq1 6660 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝑤) = (𝑏𝑤))
7877breq1d 5062 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑔𝑤)))
7976, 78anbi12d 633 . . . . . . . . . . 11 (𝑓 = 𝑏 → ((∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8079rexbidv 3289 . . . . . . . . . 10 (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8173, 80syl5bb 286 . . . . . . . . 9 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8267, 81anbi12d 633 . . . . . . . 8 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)))))
83 eleq1w 2898 . . . . . . . . . 10 (𝑔 = 𝑐 → (𝑔𝐹𝑐𝐹))
8483anbi2d 631 . . . . . . . . 9 (𝑔 = 𝑐 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑐𝐹)))
85 fveq1 6660 . . . . . . . . . . . . 13 (𝑔 = 𝑐 → (𝑔𝑦) = (𝑐𝑦))
8685eqeq2d 2835 . . . . . . . . . . . 12 (𝑔 = 𝑐 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑐𝑦)))
8786ralbidv 3192 . . . . . . . . . . 11 (𝑔 = 𝑐 → (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
88 fveq1 6660 . . . . . . . . . . . 12 (𝑔 = 𝑐 → (𝑔𝑤) = (𝑐𝑤))
8988breq2d 5064 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑏𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
9087, 89anbi12d 633 . . . . . . . . . 10 (𝑔 = 𝑐 → ((∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9190rexbidv 3289 . . . . . . . . 9 (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9284, 91anbi12d 633 . . . . . . . 8 (𝑔 = 𝑐 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))) ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
9340, 65, 82, 92, 37brab 5417 . . . . . . 7 (𝑏𝑆𝑐 ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
94 simplll 774 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑎𝐹)
95 simplrr 777 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑐𝐹)
96 an4 655 . . . . . . . . . . . . 13 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
97962rexbii 3242 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
98 reeanv 3358 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9997, 98bitri 278 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
100 eloni 6188 . . . . . . . . . . . . . 14 (𝑧 ∈ On → Ord 𝑧)
101 eloni 6188 . . . . . . . . . . . . . 14 (𝑤 ∈ On → Ord 𝑤)
102 ordtri3or 6210 . . . . . . . . . . . . . 14 ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
103100, 101, 102syl2an 598 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
104 simp1l 1194 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑧 ∈ On)
105 onelss 6220 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ On → (𝑧𝑤𝑧𝑤))
106105imp 410 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∈ On ∧ 𝑧𝑤) → 𝑧𝑤)
107106adantll 713 . . . . . . . . . . . . . . . . . . . 20 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → 𝑧𝑤)
108 ssralv 4019 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
109108anim2d 614 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦))))
110 r19.26 3165 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
111109, 110syl6ibr 255 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦))))
112 eqtr 2844 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → (𝑎𝑦) = (𝑐𝑦))
113112ralimi 3155 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
114111, 113syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
115107, 114syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
116115adantrd 495 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
1171163impia 1114 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
118 fveq2 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑏𝑦) = (𝑏𝑧))
119 fveq2 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑐𝑦) = (𝑐𝑧))
120118, 119eqeq12d 2840 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑏𝑦) = (𝑐𝑦) ↔ (𝑏𝑧) = (𝑐𝑧)))
121120rspcv 3604 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → (𝑏𝑧) = (𝑐𝑧)))
122 breq2 5056 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
123122biimpd 232 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧)))
124121, 123syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧))))
125124com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧))))
126125imp 410 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
127126ad2ant2lr 747 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
128127impcom 411 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
1291283adant1 1127 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
130 raleq 3396 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
131 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑎𝑡) = (𝑎𝑧))
132 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑐𝑡) = (𝑐𝑧))
133131, 132breq12d 5065 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
134130, 133anbi12d 633 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑧 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))))
135134rspcev 3609 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
136104, 117, 129, 135syl12anc 835 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
137136a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1381373exp 1116 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
1392orderseqlem 33154 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝐹 → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
140139ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
1412orderseqlem 33154 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝐹 → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
142141ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
1432orderseqlem 33154 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐𝐹 → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
144143ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
145140, 142, 1443jca 1125 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅})))
146 potr 5473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
1471, 145, 146sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
148147impcom 411 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (𝑎𝑧)𝑅(𝑐𝑧))
149113, 148anim12i 615 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
150149anassrs 471 . . . . . . . . . . . . . . . . . 18 (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
151150, 135sylan2 595 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
152151exp32 424 . . . . . . . . . . . . . . . 16 (𝑧 ∈ On → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
153 raleq 3396 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
154153anbi2d 631 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
155110, 154syl5bb 286 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
156 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑏𝑧) = (𝑏𝑤))
157 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑐𝑧) = (𝑐𝑤))
158156, 157breq12d 5065 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((𝑏𝑧)𝑅(𝑐𝑧) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
159158anbi2d 631 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ↔ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
160155, 159anbi12d 633 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
161160imbi1d 345 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))) ↔ (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
162152, 161syl5ibcom 248 . . . . . . . . . . . . . . 15 (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
163162adantr 484 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
164 simp1r 1195 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑤 ∈ On)
165 onelss 6220 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ On → (𝑤𝑧𝑤𝑧))
166165imp 410 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ On ∧ 𝑤𝑧) → 𝑤𝑧)
167166adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → 𝑤𝑧)
168 ssralv 4019 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦)))
169168anim1d 613 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
170 r19.26 3165 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
171112ralimi 3155 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
172170, 171sylbir 238 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
173169, 172syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
174173adantrd 495 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
175167, 174syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
1761753impia 1114 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
177 fveq2 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑎𝑦) = (𝑎𝑤))
178 fveq2 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑏𝑦) = (𝑏𝑤))
179177, 178eqeq12d 2840 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑤 → ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑎𝑤) = (𝑏𝑤)))
180179rspcv 3604 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑤) = (𝑏𝑤)))
181 breq1 5055 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑤) = (𝑏𝑤) → ((𝑎𝑤)𝑅(𝑐𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
182181biimprd 251 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑤) = (𝑏𝑤) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤)))
183180, 182syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤))))
184183com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤))))
185184imp 410 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
186185ad2ant2rl 748 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
187186impcom 411 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
1881873adant1 1127 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
189 raleq 3396 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
190 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑎𝑡) = (𝑎𝑤))
191 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑐𝑡) = (𝑐𝑤))
192190, 191breq12d 5065 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑤)𝑅(𝑐𝑤)))
193189, 192anbi12d 633 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑤 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))))
194193rspcev 3609 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ On ∧ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
195164, 176, 188, 194syl12anc 835 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
196195a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1971963exp 1116 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
198138, 163, 1973jaod 1425 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧𝑤𝑧 = 𝑤𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
199103, 198mpd 15 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
200199rexlimivv 3284 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20199, 200sylbir 238 . . . . . . . . . 10 ((∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
202201impcom 411 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
20394, 95, 202jca31 518 . . . . . . . 8 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
204203an4s 659 . . . . . . 7 ((((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))) ∧ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20564, 93, 204syl2anb 600 . . . . . 6 ((𝑎𝑆𝑏𝑏𝑆𝑐) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
206 raleq 3396 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦)))
207 fveq2 6661 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑓𝑥) = (𝑓𝑡))
208 fveq2 6661 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
209207, 208breq12d 5065 . . . . . . . . . . 11 (𝑥 = 𝑡 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑡)𝑅(𝑔𝑡)))
210206, 209anbi12d 633 . . . . . . . . . 10 (𝑥 = 𝑡 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡))))
211210cbvrexvw 3435 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)))
21220ralbidv 3192 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦)))
213 fveq1 6660 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑡) = (𝑎𝑡))
214213breq1d 5062 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑔𝑡)))
215212, 214anbi12d 633 . . . . . . . . . 10 (𝑓 = 𝑎 → ((∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
216215rexbidv 3289 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
217211, 216syl5bb 286 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
21818, 217anbi12d 633 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)))))
21983anbi2d 631 . . . . . . . 8 (𝑔 = 𝑐 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑐𝐹)))
22085eqeq2d 2835 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑐𝑦)))
221220ralbidv 3192 . . . . . . . . . 10 (𝑔 = 𝑐 → (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦)))
222 fveq1 6660 . . . . . . . . . . 11 (𝑔 = 𝑐 → (𝑔𝑡) = (𝑐𝑡))
223222breq2d 5064 . . . . . . . . . 10 (𝑔 = 𝑐 → ((𝑎𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑐𝑡)))
224221, 223anbi12d 633 . . . . . . . . 9 (𝑔 = 𝑐 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
225224rexbidv 3289 . . . . . . . 8 (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
226219, 225anbi12d 633 . . . . . . 7 (𝑔 = 𝑐 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))) ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
22716, 65, 218, 226, 37brab 5417 . . . . . 6 (𝑎𝑆𝑐 ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
228205, 227sylibr 237 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)
22939, 228pm3.2i 474 . . . 4 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230229a1i 11 . . 3 ((𝑎𝐹𝑏𝐹𝑐𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231230rgen3 3199 . 2 𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232 df-po 5461 . 2 (𝑆 Po 𝐹 ↔ ∀𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233231, 232mpbir 234 1 𝑆 Po 𝐹
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ w3o 1083   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115  {cab 2802  ∀wral 3133  ∃wrex 3134   ∪ cun 3917   ⊆ wss 3919  ∅c0 4276  {csn 4550   class class class wbr 5052  {copab 5114   Po wpo 5459  Ord word 6177  Oncon0 6178  ⟶wf 6339  ‘cfv 6343 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-tr 5159  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-ord 6181  df-on 6182  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-fv 6351 This theorem is referenced by:  soseq  33156
 Copyright terms: Public domain W3C validator