MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  poseq Structured version   Visualization version   GIF version

Theorem poseq 8139
Description: A partial ordering of ordinal sequences. (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 6690 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑏 → (𝑓:𝑥𝐴𝑓:𝑏𝐴))
43cbvrexvw 3227 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏𝐴)
54abbii 2794 . . . . . . . . . . . . . 14 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
62, 5eqtri 2752 . . . . . . . . . . . . 13 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
76orderseqlem 8138 . . . . . . . . . . . 12 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
8 poirr 5591 . . . . . . . . . . . 12 ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
91, 7, 8sylancr 586 . . . . . . . . . . 11 (𝑎𝐹 → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
109intnand 488 . . . . . . . . . 10 (𝑎𝐹 → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1110adantr 480 . . . . . . . . 9 ((𝑎𝐹𝑥 ∈ On) → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1211nrexdv 3141 . . . . . . . 8 (𝑎𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1312adantr 480 . . . . . . 7 ((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
14 imnan 399 . . . . . . 7 (((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))) ↔ ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
1513, 14mpbi 229 . . . . . 6 ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
16 vex 3470 . . . . . . 7 𝑎 ∈ V
17 eleq1w 2808 . . . . . . . . 9 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
1817anbi1d 629 . . . . . . . 8 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
19 fveq1 6881 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
2019eqeq1d 2726 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
2120ralbidv 3169 . . . . . . . . . 10 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
22 fveq1 6881 . . . . . . . . . . 11 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
2322breq1d 5149 . . . . . . . . . 10 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
2421, 23anbi12d 630 . . . . . . . . 9 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2524rexbidv 3170 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2618, 25anbi12d 630 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
27 eleq1w 2808 . . . . . . . . 9 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
2827anbi2d 628 . . . . . . . 8 (𝑔 = 𝑎 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑎𝐹)))
29 fveq1 6881 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
3029eqeq2d 2735 . . . . . . . . . . 11 (𝑔 = 𝑎 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑎𝑦)))
3130ralbidv 3169 . . . . . . . . . 10 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦)))
32 fveq1 6881 . . . . . . . . . . 11 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
3332breq2d 5151 . . . . . . . . . 10 (𝑔 = 𝑎 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑎𝑥)))
3431, 33anbi12d 630 . . . . . . . . 9 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3534rexbidv 3170 . . . . . . . 8 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3628, 35anbi12d 630 . . . . . . 7 (𝑔 = 𝑎 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))))
37 poseq.3 . . . . . . 7 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
3816, 16, 26, 36, 37brab 5534 . . . . . 6 (𝑎𝑆𝑎 ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3915, 38mtbir 323 . . . . 5 ¬ 𝑎𝑆𝑎
40 vex 3470 . . . . . . . 8 𝑏 ∈ V
41 raleq 3314 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦)))
42 fveq2 6882 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓𝑥) = (𝑓𝑧))
43 fveq2 6882 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑔𝑥) = (𝑔𝑧))
4442, 43breq12d 5152 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑧)𝑅(𝑔𝑧)))
4541, 44anbi12d 630 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧))))
4645cbvrexvw 3227 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)))
4720ralbidv 3169 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦)))
48 fveq1 6881 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (𝑓𝑧) = (𝑎𝑧))
4948breq1d 5149 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((𝑓𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑔𝑧)))
5047, 49anbi12d 630 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5150rexbidv 3170 . . . . . . . . . 10 (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5246, 51bitrid 283 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5318, 52anbi12d 630 . . . . . . . 8 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)))))
54 eleq1w 2808 . . . . . . . . . 10 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
5554anbi2d 628 . . . . . . . . 9 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
56 fveq1 6881 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
5756eqeq2d 2735 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
5857ralbidv 3169 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦)))
59 fveq1 6881 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝑧) = (𝑏𝑧))
6059breq2d 5151 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑏𝑧)))
6158, 60anbi12d 630 . . . . . . . . . 10 (𝑔 = 𝑏 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6261rexbidv 3170 . . . . . . . . 9 (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6355, 62anbi12d 630 . . . . . . . 8 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)))))
6416, 40, 53, 63, 37brab 5534 . . . . . . 7 (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
65 vex 3470 . . . . . . . 8 𝑐 ∈ V
66 eleq1w 2808 . . . . . . . . . 10 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
6766anbi1d 629 . . . . . . . . 9 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
68 raleq 3314 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦)))
69 fveq2 6882 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑓𝑥) = (𝑓𝑤))
70 fveq2 6882 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑔𝑥) = (𝑔𝑤))
7169, 70breq12d 5152 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑤)𝑅(𝑔𝑤)))
7268, 71anbi12d 630 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤))))
7372cbvrexvw 3227 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)))
74 fveq1 6881 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
7574eqeq1d 2726 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
7675ralbidv 3169 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦)))
77 fveq1 6881 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝑤) = (𝑏𝑤))
7877breq1d 5149 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑔𝑤)))
7976, 78anbi12d 630 . . . . . . . . . . 11 (𝑓 = 𝑏 → ((∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8079rexbidv 3170 . . . . . . . . . 10 (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8173, 80bitrid 283 . . . . . . . . 9 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8267, 81anbi12d 630 . . . . . . . 8 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)))))
83 eleq1w 2808 . . . . . . . . . 10 (𝑔 = 𝑐 → (𝑔𝐹𝑐𝐹))
8483anbi2d 628 . . . . . . . . 9 (𝑔 = 𝑐 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑐𝐹)))
85 fveq1 6881 . . . . . . . . . . . . 13 (𝑔 = 𝑐 → (𝑔𝑦) = (𝑐𝑦))
8685eqeq2d 2735 . . . . . . . . . . . 12 (𝑔 = 𝑐 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑐𝑦)))
8786ralbidv 3169 . . . . . . . . . . 11 (𝑔 = 𝑐 → (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
88 fveq1 6881 . . . . . . . . . . . 12 (𝑔 = 𝑐 → (𝑔𝑤) = (𝑐𝑤))
8988breq2d 5151 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑏𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
9087, 89anbi12d 630 . . . . . . . . . 10 (𝑔 = 𝑐 → ((∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9190rexbidv 3170 . . . . . . . . 9 (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9284, 91anbi12d 630 . . . . . . . 8 (𝑔 = 𝑐 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))) ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
9340, 65, 82, 92, 37brab 5534 . . . . . . 7 (𝑏𝑆𝑐 ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
94 simplll 772 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑎𝐹)
95 simplrr 775 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑐𝐹)
96 an4 653 . . . . . . . . . . . . 13 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
97962rexbii 3121 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
98 reeanv 3218 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9997, 98bitri 275 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
100 eloni 6365 . . . . . . . . . . . . . 14 (𝑧 ∈ On → Ord 𝑧)
101 eloni 6365 . . . . . . . . . . . . . 14 (𝑤 ∈ On → Ord 𝑤)
102 ordtri3or 6387 . . . . . . . . . . . . . 14 ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
103100, 101, 102syl2an 595 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
104 simp1l 1194 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑧 ∈ On)
105 onelss 6397 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ On → (𝑧𝑤𝑧𝑤))
106105imp 406 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∈ On ∧ 𝑧𝑤) → 𝑧𝑤)
107106adantll 711 . . . . . . . . . . . . . . . . . . . 20 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → 𝑧𝑤)
108 ssralv 4043 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
109108anim2d 611 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦))))
110 r19.26 3103 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
111109, 110imbitrrdi 251 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦))))
112 eqtr 2747 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → (𝑎𝑦) = (𝑐𝑦))
113112ralimi 3075 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
114111, 113syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
115107, 114syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
116115adantrd 491 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
1171163impia 1114 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
118 fveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑏𝑦) = (𝑏𝑧))
119 fveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑐𝑦) = (𝑐𝑧))
120118, 119eqeq12d 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑏𝑦) = (𝑐𝑦) ↔ (𝑏𝑧) = (𝑐𝑧)))
121120rspcv 3600 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → (𝑏𝑧) = (𝑐𝑧)))
122 breq2 5143 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
123122biimpd 228 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧)))
124121, 123syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧))))
125124com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧))))
126125imp 406 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
127126ad2ant2lr 745 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
128127impcom 407 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
1291283adant1 1127 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
130 raleq 3314 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
131 fveq2 6882 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑎𝑡) = (𝑎𝑧))
132 fveq2 6882 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑐𝑡) = (𝑐𝑧))
133131, 132breq12d 5152 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
134130, 133anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑧 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))))
135134rspcev 3604 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
136104, 117, 129, 135syl12anc 834 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
137136a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1381373exp 1116 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
1392orderseqlem 8138 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝐹 → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
140139ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
1412orderseqlem 8138 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝐹 → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
142141ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
1432orderseqlem 8138 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐𝐹 → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
144143ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
145140, 142, 1443jca 1125 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅})))
146 potr 5592 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
1471, 145, 146sylancr 586 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
148147impcom 407 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (𝑎𝑧)𝑅(𝑐𝑧))
149113, 148anim12i 612 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
150149anassrs 467 . . . . . . . . . . . . . . . . . 18 (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
151150, 135sylan2 592 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
152151exp32 420 . . . . . . . . . . . . . . . 16 (𝑧 ∈ On → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
153 raleq 3314 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
154153anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
155110, 154bitrid 283 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
156 fveq2 6882 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑏𝑧) = (𝑏𝑤))
157 fveq2 6882 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑐𝑧) = (𝑐𝑤))
158156, 157breq12d 5152 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((𝑏𝑧)𝑅(𝑐𝑧) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
159158anbi2d 628 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ↔ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
160155, 159anbi12d 630 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
161160imbi1d 341 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))) ↔ (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
162152, 161syl5ibcom 244 . . . . . . . . . . . . . . 15 (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
163162adantr 480 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
164 simp1r 1195 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑤 ∈ On)
165 onelss 6397 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ On → (𝑤𝑧𝑤𝑧))
166165imp 406 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ On ∧ 𝑤𝑧) → 𝑤𝑧)
167166adantlr 712 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → 𝑤𝑧)
168 ssralv 4043 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦)))
169168anim1d 610 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
170 r19.26 3103 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
171112ralimi 3075 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
172170, 171sylbir 234 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
173169, 172syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
174173adantrd 491 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
175167, 174syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
1761753impia 1114 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
177 fveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑎𝑦) = (𝑎𝑤))
178 fveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑏𝑦) = (𝑏𝑤))
179177, 178eqeq12d 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑤 → ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑎𝑤) = (𝑏𝑤)))
180179rspcv 3600 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑤) = (𝑏𝑤)))
181 breq1 5142 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑤) = (𝑏𝑤) → ((𝑎𝑤)𝑅(𝑐𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
182181biimprd 247 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑤) = (𝑏𝑤) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤)))
183180, 182syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤))))
184183com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤))))
185184imp 406 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
186185ad2ant2rl 746 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
187186impcom 407 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
1881873adant1 1127 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
189 raleq 3314 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
190 fveq2 6882 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑎𝑡) = (𝑎𝑤))
191 fveq2 6882 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑐𝑡) = (𝑐𝑤))
192190, 191breq12d 5152 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑤)𝑅(𝑐𝑤)))
193189, 192anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑤 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))))
194193rspcev 3604 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ On ∧ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
195164, 176, 188, 194syl12anc 834 . . . . . . . . . . . . . . . 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 3191 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20199, 200sylbir 234 . . . . . . . . . 10 ((∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
202201impcom 407 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
20394, 95, 202jca31 514 . . . . . . . 8 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
204203an4s 657 . . . . . . 7 ((((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))) ∧ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20564, 93, 204syl2anb 597 . . . . . 6 ((𝑎𝑆𝑏𝑏𝑆𝑐) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
206 raleq 3314 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦)))
207 fveq2 6882 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑓𝑥) = (𝑓𝑡))
208 fveq2 6882 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
209207, 208breq12d 5152 . . . . . . . . . . 11 (𝑥 = 𝑡 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑡)𝑅(𝑔𝑡)))
210206, 209anbi12d 630 . . . . . . . . . 10 (𝑥 = 𝑡 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡))))
211210cbvrexvw 3227 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)))
21220ralbidv 3169 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦)))
213 fveq1 6881 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑡) = (𝑎𝑡))
214213breq1d 5149 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑔𝑡)))
215212, 214anbi12d 630 . . . . . . . . . 10 (𝑓 = 𝑎 → ((∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
216215rexbidv 3170 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
217211, 216bitrid 283 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
21818, 217anbi12d 630 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)))))
21983anbi2d 628 . . . . . . . 8 (𝑔 = 𝑐 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑐𝐹)))
22085eqeq2d 2735 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑐𝑦)))
221220ralbidv 3169 . . . . . . . . . 10 (𝑔 = 𝑐 → (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦)))
222 fveq1 6881 . . . . . . . . . . 11 (𝑔 = 𝑐 → (𝑔𝑡) = (𝑐𝑡))
223222breq2d 5151 . . . . . . . . . 10 (𝑔 = 𝑐 → ((𝑎𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑐𝑡)))
224221, 223anbi12d 630 . . . . . . . . 9 (𝑔 = 𝑐 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
225224rexbidv 3170 . . . . . . . 8 (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
226219, 225anbi12d 630 . . . . . . 7 (𝑔 = 𝑐 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))) ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
22716, 65, 218, 226, 37brab 5534 . . . . . 6 (𝑎𝑆𝑐 ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
228205, 227sylibr 233 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)
22939, 228pm3.2i 470 . . . 4 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230229a1i 11 . . 3 ((𝑎𝐹𝑏𝐹𝑐𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231230rgen3 3194 . 2 𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232 df-po 5579 . 2 (𝑆 Po 𝐹 ↔ ∀𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233231, 232mpbir 230 1 𝑆 Po 𝐹
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3o 1083  w3a 1084   = wceq 1533  wcel 2098  {cab 2701  wral 3053  wrex 3062  cun 3939  wss 3941  c0 4315  {csn 4621   class class class wbr 5139  {copab 5201   Po wpo 5577  Ord word 6354  Oncon0 6355  wf 6530  cfv 6534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-tr 5257  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-ord 6358  df-on 6359  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-fv 6542
This theorem is referenced by:  soseq  8140
  Copyright terms: Public domain W3C validator