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 32090
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 6167 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑏 → (𝑓:𝑥𝐴𝑓:𝑏𝐴))
43cbvrexv 3321 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏𝐴)
54abbii 2888 . . . . . . . . . . . . . 14 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
62, 5eqtri 2793 . . . . . . . . . . . . 13 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
76orderseqlem 32089 . . . . . . . . . . . 12 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
8 poirr 5181 . . . . . . . . . . . 12 ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
91, 7, 8sylancr 575 . . . . . . . . . . 11 (𝑎𝐹 → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
109intnand 476 . . . . . . . . . 10 (𝑎𝐹 → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1110adantr 466 . . . . . . . . 9 ((𝑎𝐹𝑥 ∈ On) → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1211nrexdv 3149 . . . . . . . 8 (𝑎𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1312adantr 466 . . . . . . 7 ((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
14 imnan 386 . . . . . . 7 (((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))) ↔ ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
1513, 14mpbi 220 . . . . . 6 ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
16 vex 3354 . . . . . . 7 𝑎 ∈ V
17 eleq1w 2833 . . . . . . . . 9 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
1817anbi1d 615 . . . . . . . 8 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
19 fveq1 6331 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
2019eqeq1d 2773 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
2120ralbidv 3135 . . . . . . . . . 10 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
22 fveq1 6331 . . . . . . . . . . 11 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
2322breq1d 4796 . . . . . . . . . 10 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
2421, 23anbi12d 616 . . . . . . . . 9 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2524rexbidv 3200 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2618, 25anbi12d 616 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
27 eleq1w 2833 . . . . . . . . 9 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
2827anbi2d 614 . . . . . . . 8 (𝑔 = 𝑎 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑎𝐹)))
29 fveq1 6331 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
3029eqeq2d 2781 . . . . . . . . . . 11 (𝑔 = 𝑎 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑎𝑦)))
3130ralbidv 3135 . . . . . . . . . 10 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦)))
32 fveq1 6331 . . . . . . . . . . 11 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
3332breq2d 4798 . . . . . . . . . 10 (𝑔 = 𝑎 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑎𝑥)))
3431, 33anbi12d 616 . . . . . . . . 9 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3534rexbidv 3200 . . . . . . . 8 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3628, 35anbi12d 616 . . . . . . 7 (𝑔 = 𝑎 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))))
37 poseq.3 . . . . . . 7 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
3816, 16, 26, 36, 37brab 5131 . . . . . 6 (𝑎𝑆𝑎 ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3915, 38mtbir 312 . . . . 5 ¬ 𝑎𝑆𝑎
40 vex 3354 . . . . . . . 8 𝑏 ∈ V
41 raleq 3287 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦)))
42 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓𝑥) = (𝑓𝑧))
43 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑔𝑥) = (𝑔𝑧))
4442, 43breq12d 4799 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑧)𝑅(𝑔𝑧)))
4541, 44anbi12d 616 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧))))
4645cbvrexv 3321 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)))
4720ralbidv 3135 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦)))
48 fveq1 6331 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (𝑓𝑧) = (𝑎𝑧))
4948breq1d 4796 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((𝑓𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑔𝑧)))
5047, 49anbi12d 616 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5150rexbidv 3200 . . . . . . . . . 10 (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5246, 51syl5bb 272 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5318, 52anbi12d 616 . . . . . . . 8 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)))))
54 eleq1w 2833 . . . . . . . . . 10 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
5554anbi2d 614 . . . . . . . . 9 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
56 fveq1 6331 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
5756eqeq2d 2781 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
5857ralbidv 3135 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦)))
59 fveq1 6331 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝑧) = (𝑏𝑧))
6059breq2d 4798 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑏𝑧)))
6158, 60anbi12d 616 . . . . . . . . . 10 (𝑔 = 𝑏 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6261rexbidv 3200 . . . . . . . . 9 (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6355, 62anbi12d 616 . . . . . . . 8 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)))))
6416, 40, 53, 63, 37brab 5131 . . . . . . 7 (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
65 vex 3354 . . . . . . . 8 𝑐 ∈ V
66 eleq1w 2833 . . . . . . . . . 10 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
6766anbi1d 615 . . . . . . . . 9 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
68 raleq 3287 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦)))
69 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑓𝑥) = (𝑓𝑤))
70 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑔𝑥) = (𝑔𝑤))
7169, 70breq12d 4799 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑤)𝑅(𝑔𝑤)))
7268, 71anbi12d 616 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤))))
7372cbvrexv 3321 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)))
74 fveq1 6331 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
7574eqeq1d 2773 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
7675ralbidv 3135 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦)))
77 fveq1 6331 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝑤) = (𝑏𝑤))
7877breq1d 4796 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑔𝑤)))
7976, 78anbi12d 616 . . . . . . . . . . 11 (𝑓 = 𝑏 → ((∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8079rexbidv 3200 . . . . . . . . . 10 (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8173, 80syl5bb 272 . . . . . . . . 9 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8267, 81anbi12d 616 . . . . . . . 8 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)))))
83 eleq1w 2833 . . . . . . . . . 10 (𝑔 = 𝑐 → (𝑔𝐹𝑐𝐹))
8483anbi2d 614 . . . . . . . . 9 (𝑔 = 𝑐 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑐𝐹)))
85 fveq1 6331 . . . . . . . . . . . . 13 (𝑔 = 𝑐 → (𝑔𝑦) = (𝑐𝑦))
8685eqeq2d 2781 . . . . . . . . . . . 12 (𝑔 = 𝑐 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑐𝑦)))
8786ralbidv 3135 . . . . . . . . . . 11 (𝑔 = 𝑐 → (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
88 fveq1 6331 . . . . . . . . . . . 12 (𝑔 = 𝑐 → (𝑔𝑤) = (𝑐𝑤))
8988breq2d 4798 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑏𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
9087, 89anbi12d 616 . . . . . . . . . 10 (𝑔 = 𝑐 → ((∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9190rexbidv 3200 . . . . . . . . 9 (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9284, 91anbi12d 616 . . . . . . . 8 (𝑔 = 𝑐 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))) ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
9340, 65, 82, 92, 37brab 5131 . . . . . . 7 (𝑏𝑆𝑐 ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
94 simplll 758 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑎𝐹)
95 simplrr 763 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑐𝐹)
96 an4 635 . . . . . . . . . . . . 13 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
97962rexbii 3190 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
98 reeanv 3255 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9997, 98bitri 264 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
100 eloni 5876 . . . . . . . . . . . . . 14 (𝑧 ∈ On → Ord 𝑧)
101 eloni 5876 . . . . . . . . . . . . . 14 (𝑤 ∈ On → Ord 𝑤)
102 ordtri3or 5898 . . . . . . . . . . . . . 14 ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
103100, 101, 102syl2an 583 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
104 simp1l 1239 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑧 ∈ On)
105 onelss 5909 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ On → (𝑧𝑤𝑧𝑤))
106105imp 393 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∈ On ∧ 𝑧𝑤) → 𝑧𝑤)
107106adantll 693 . . . . . . . . . . . . . . . . . . . 20 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → 𝑧𝑤)
108 ssralv 3815 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
109108anim2d 599 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦))))
110 r19.26 3212 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
111109, 110syl6ibr 242 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦))))
112 eqtr 2790 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → (𝑎𝑦) = (𝑐𝑦))
113112ralimi 3101 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
114111, 113syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
115107, 114syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
116115adantrd 479 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
1171163impia 1109 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
118 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑏𝑦) = (𝑏𝑧))
119 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑐𝑦) = (𝑐𝑧))
120118, 119eqeq12d 2786 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑏𝑦) = (𝑐𝑦) ↔ (𝑏𝑧) = (𝑐𝑧)))
121120rspcv 3456 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → (𝑏𝑧) = (𝑐𝑧)))
122 breq2 4790 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
123122biimpd 219 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧)))
124121, 123syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧))))
125124com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧))))
126125imp 393 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
127126ad2ant2lr 742 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
128127impcom 394 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
1291283adant1 1124 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
130 raleq 3287 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
131 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑎𝑡) = (𝑎𝑧))
132 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑐𝑡) = (𝑐𝑧))
133131, 132breq12d 4799 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
134130, 133anbi12d 616 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑧 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))))
135134rspcev 3460 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
136104, 117, 129, 135syl12anc 1474 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
137136a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1381373exp 1112 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
1392orderseqlem 32089 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝐹 → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
140139ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
1412orderseqlem 32089 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝐹 → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
142141ad2antlr 706 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
1432orderseqlem 32089 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐𝐹 → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
144143ad2antll 708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
145140, 142, 1443jca 1122 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅})))
146 potr 5182 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
1471, 145, 146sylancr 575 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
148147impcom 394 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (𝑎𝑧)𝑅(𝑐𝑧))
149113, 148anim12i 600 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
150149anassrs 458 . . . . . . . . . . . . . . . . . 18 (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
151150, 135sylan2 580 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
152151exp32 407 . . . . . . . . . . . . . . . 16 (𝑧 ∈ On → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
153 raleq 3287 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
154153anbi2d 614 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
155110, 154syl5bb 272 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
156 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑏𝑧) = (𝑏𝑤))
157 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑐𝑧) = (𝑐𝑤))
158156, 157breq12d 4799 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((𝑏𝑧)𝑅(𝑐𝑧) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
159158anbi2d 614 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ↔ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
160155, 159anbi12d 616 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
161160imbi1d 330 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))) ↔ (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
162152, 161syl5ibcom 235 . . . . . . . . . . . . . . 15 (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
163162adantr 466 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
164 simp1r 1240 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑤 ∈ On)
165 onelss 5909 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ On → (𝑤𝑧𝑤𝑧))
166165imp 393 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ On ∧ 𝑤𝑧) → 𝑤𝑧)
167166adantlr 694 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → 𝑤𝑧)
168 ssralv 3815 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦)))
169168anim1d 598 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
170 r19.26 3212 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
171112ralimi 3101 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
172170, 171sylbir 225 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
173169, 172syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
174173adantrd 479 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
175167, 174syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
1761753impia 1109 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
177 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑎𝑦) = (𝑎𝑤))
178 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑏𝑦) = (𝑏𝑤))
179177, 178eqeq12d 2786 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑤 → ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑎𝑤) = (𝑏𝑤)))
180179rspcv 3456 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑤) = (𝑏𝑤)))
181 breq1 4789 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑤) = (𝑏𝑤) → ((𝑎𝑤)𝑅(𝑐𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
182181biimprd 238 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑤) = (𝑏𝑤) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤)))
183180, 182syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤))))
184183com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤))))
185184imp 393 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
186185ad2ant2rl 743 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
187186impcom 394 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
1881873adant1 1124 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
189 raleq 3287 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
190 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑎𝑡) = (𝑎𝑤))
191 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑐𝑡) = (𝑐𝑤))
192190, 191breq12d 4799 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑤)𝑅(𝑐𝑤)))
193189, 192anbi12d 616 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑤 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))))
194193rspcev 3460 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ On ∧ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
195164, 176, 188, 194syl12anc 1474 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
196195a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1971963exp 1112 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
198138, 163, 1973jaod 1540 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧𝑤𝑧 = 𝑤𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
199103, 198mpd 15 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
200199rexlimivv 3184 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20199, 200sylbir 225 . . . . . . . . . 10 ((∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
202201impcom 394 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
20394, 95, 202jca31 504 . . . . . . . 8 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
204203an4s 639 . . . . . . 7 ((((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))) ∧ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20564, 93, 204syl2anb 585 . . . . . 6 ((𝑎𝑆𝑏𝑏𝑆𝑐) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
206 raleq 3287 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦)))
207 fveq2 6332 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑓𝑥) = (𝑓𝑡))
208 fveq2 6332 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
209207, 208breq12d 4799 . . . . . . . . . . 11 (𝑥 = 𝑡 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑡)𝑅(𝑔𝑡)))
210206, 209anbi12d 616 . . . . . . . . . 10 (𝑥 = 𝑡 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡))))
211210cbvrexv 3321 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)))
21220ralbidv 3135 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦)))
213 fveq1 6331 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑡) = (𝑎𝑡))
214213breq1d 4796 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑔𝑡)))
215212, 214anbi12d 616 . . . . . . . . . 10 (𝑓 = 𝑎 → ((∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
216215rexbidv 3200 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
217211, 216syl5bb 272 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
21818, 217anbi12d 616 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)))))
21983anbi2d 614 . . . . . . . 8 (𝑔 = 𝑐 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑐𝐹)))
22085eqeq2d 2781 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑐𝑦)))
221220ralbidv 3135 . . . . . . . . . 10 (𝑔 = 𝑐 → (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦)))
222 fveq1 6331 . . . . . . . . . . 11 (𝑔 = 𝑐 → (𝑔𝑡) = (𝑐𝑡))
223222breq2d 4798 . . . . . . . . . 10 (𝑔 = 𝑐 → ((𝑎𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑐𝑡)))
224221, 223anbi12d 616 . . . . . . . . 9 (𝑔 = 𝑐 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
225224rexbidv 3200 . . . . . . . 8 (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
226219, 225anbi12d 616 . . . . . . 7 (𝑔 = 𝑐 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))) ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
22716, 65, 218, 226, 37brab 5131 . . . . . 6 (𝑎𝑆𝑐 ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
228205, 227sylibr 224 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)
22939, 228pm3.2i 447 . . . 4 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230229a1i 11 . . 3 ((𝑎𝐹𝑏𝐹𝑐𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231230rgen3 3125 . 2 𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232 df-po 5170 . 2 (𝑆 Po 𝐹 ↔ ∀𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233231, 232mpbir 221 1 𝑆 Po 𝐹
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3o 1070  w3a 1071   = wceq 1631  wcel 2145  {cab 2757  wral 3061  wrex 3062  cun 3721  wss 3723  c0 4063  {csn 4316   class class class wbr 4786  {copab 4846   Po wpo 5168  Ord word 5865  Oncon0 5866  wf 6027  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-tr 4887  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-ord 5869  df-on 5870  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039
This theorem is referenced by:  soseq  32091
  Copyright terms: Public domain W3C validator