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 31451
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 5984 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑏 → (𝑓:𝑥𝐴𝑓:𝑏𝐴))
43cbvrexv 3160 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏𝐴)
54abbii 2736 . . . . . . . . . . . . . 14 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
62, 5eqtri 2643 . . . . . . . . . . . . 13 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏𝐴}
76orderseqlem 31450 . . . . . . . . . . . 12 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
8 poirr 5006 . . . . . . . . . . . 12 ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
91, 7, 8sylancr 694 . . . . . . . . . . 11 (𝑎𝐹 → ¬ (𝑎𝑥)𝑅(𝑎𝑥))
109intnand 961 . . . . . . . . . 10 (𝑎𝐹 → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1110adantr 481 . . . . . . . . 9 ((𝑎𝐹𝑥 ∈ On) → ¬ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1211nrexdv 2995 . . . . . . . 8 (𝑎𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
1312adantr 481 . . . . . . 7 ((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
14 imnan 438 . . . . . . 7 (((𝑎𝐹𝑎𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))) ↔ ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
1513, 14mpbi 220 . . . . . 6 ¬ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))
16 vex 3189 . . . . . . 7 𝑎 ∈ V
17 eleq1 2686 . . . . . . . . 9 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
1817anbi1d 740 . . . . . . . 8 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
19 fveq1 6147 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
2019eqeq1d 2623 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
2120ralbidv 2980 . . . . . . . . . 10 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
22 fveq1 6147 . . . . . . . . . . 11 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
2322breq1d 4623 . . . . . . . . . 10 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
2421, 23anbi12d 746 . . . . . . . . 9 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2524rexbidv 3045 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
2618, 25anbi12d 746 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
27 eleq1 2686 . . . . . . . . 9 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
2827anbi2d 739 . . . . . . . 8 (𝑔 = 𝑎 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑎𝐹)))
29 fveq1 6147 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
3029eqeq2d 2631 . . . . . . . . . . 11 (𝑔 = 𝑎 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑎𝑦)))
3130ralbidv 2980 . . . . . . . . . 10 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦)))
32 fveq1 6147 . . . . . . . . . . 11 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
3332breq2d 4625 . . . . . . . . . 10 (𝑔 = 𝑎 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑎𝑥)))
3431, 33anbi12d 746 . . . . . . . . 9 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3534rexbidv 3045 . . . . . . . 8 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3628, 35anbi12d 746 . . . . . . 7 (𝑔 = 𝑎 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥)))))
37 poseq.3 . . . . . . 7 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
3816, 16, 26, 36, 37brab 4958 . . . . . 6 (𝑎𝑆𝑎 ↔ ((𝑎𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑎𝑦) ∧ (𝑎𝑥)𝑅(𝑎𝑥))))
3915, 38mtbir 313 . . . . 5 ¬ 𝑎𝑆𝑎
40 vex 3189 . . . . . . . 8 𝑏 ∈ V
41 raleq 3127 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦)))
42 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓𝑥) = (𝑓𝑧))
43 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑔𝑥) = (𝑔𝑧))
4442, 43breq12d 4626 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑧)𝑅(𝑔𝑧)))
4541, 44anbi12d 746 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧))))
4645cbvrexv 3160 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)))
4720ralbidv 2980 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦)))
48 fveq1 6147 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (𝑓𝑧) = (𝑎𝑧))
4948breq1d 4623 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((𝑓𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑔𝑧)))
5047, 49anbi12d 746 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5150rexbidv 3045 . . . . . . . . . 10 (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5246, 51syl5bb 272 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))))
5318, 52anbi12d 746 . . . . . . . 8 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)))))
54 eleq1 2686 . . . . . . . . . 10 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
5554anbi2d 739 . . . . . . . . 9 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
56 fveq1 6147 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
5756eqeq2d 2631 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
5857ralbidv 2980 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦)))
59 fveq1 6147 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝑧) = (𝑏𝑧))
6059breq2d 4625 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝑧)𝑅(𝑔𝑧) ↔ (𝑎𝑧)𝑅(𝑏𝑧)))
6158, 60anbi12d 746 . . . . . . . . . 10 (𝑔 = 𝑏 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6261rexbidv 3045 . . . . . . . . 9 (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
6355, 62anbi12d 746 . . . . . . . 8 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑧)𝑅(𝑔𝑧))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)))))
6416, 40, 53, 63, 37brab 4958 . . . . . . 7 (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))))
65 vex 3189 . . . . . . . 8 𝑐 ∈ V
66 eleq1 2686 . . . . . . . . . 10 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
6766anbi1d 740 . . . . . . . . 9 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
68 raleq 3127 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦)))
69 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑓𝑥) = (𝑓𝑤))
70 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑔𝑥) = (𝑔𝑤))
7169, 70breq12d 4626 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑤)𝑅(𝑔𝑤)))
7268, 71anbi12d 746 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤))))
7372cbvrexv 3160 . . . . . . . . . 10 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)))
74 fveq1 6147 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
7574eqeq1d 2623 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
7675ralbidv 2980 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦)))
77 fveq1 6147 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝑤) = (𝑏𝑤))
7877breq1d 4623 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑔𝑤)))
7976, 78anbi12d 746 . . . . . . . . . . 11 (𝑓 = 𝑏 → ((∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8079rexbidv 3045 . . . . . . . . . 10 (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8173, 80syl5bb 272 . . . . . . . . 9 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))))
8267, 81anbi12d 746 . . . . . . . 8 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)))))
83 eleq1 2686 . . . . . . . . . 10 (𝑔 = 𝑐 → (𝑔𝐹𝑐𝐹))
8483anbi2d 739 . . . . . . . . 9 (𝑔 = 𝑐 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑐𝐹)))
85 fveq1 6147 . . . . . . . . . . . . 13 (𝑔 = 𝑐 → (𝑔𝑦) = (𝑐𝑦))
8685eqeq2d 2631 . . . . . . . . . . . 12 (𝑔 = 𝑐 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑐𝑦)))
8786ralbidv 2980 . . . . . . . . . . 11 (𝑔 = 𝑐 → (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
88 fveq1 6147 . . . . . . . . . . . 12 (𝑔 = 𝑐 → (𝑔𝑤) = (𝑐𝑤))
8988breq2d 4625 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑏𝑤)𝑅(𝑔𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
9087, 89anbi12d 746 . . . . . . . . . 10 (𝑔 = 𝑐 → ((∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9190rexbidv 3045 . . . . . . . . 9 (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9284, 91anbi12d 746 . . . . . . . 8 (𝑔 = 𝑐 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑤)𝑅(𝑔𝑤))) ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
9340, 65, 82, 92, 37brab 4958 . . . . . . 7 (𝑏𝑆𝑐 ↔ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
94 simplll 797 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑎𝐹)
95 simplrr 800 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑐𝐹)
96 an4 864 . . . . . . . . . . . . 13 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
97962rexbii 3035 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
98 reeanv 3097 . . . . . . . . . . . 12 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
9997, 98bitri 264 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
100 eloni 5692 . . . . . . . . . . . . . 14 (𝑧 ∈ On → Ord 𝑧)
101 eloni 5692 . . . . . . . . . . . . . 14 (𝑤 ∈ On → Ord 𝑤)
102 ordtri3or 5714 . . . . . . . . . . . . . 14 ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
103100, 101, 102syl2an 494 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
104 simp1l 1083 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑧 ∈ On)
105 onelss 5725 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ On → (𝑧𝑤𝑧𝑤))
106105imp 445 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∈ On ∧ 𝑧𝑤) → 𝑧𝑤)
107106adantll 749 . . . . . . . . . . . . . . . . . . . 20 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → 𝑧𝑤)
108 ssralv 3645 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
109108anim2d 588 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦))))
110 r19.26 3057 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)))
111109, 110syl6ibr 242 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦))))
112 eqtr 2640 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → (𝑎𝑦) = (𝑐𝑦))
113112ralimi 2947 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
114111, 113syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
115107, 114syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
116115adantrd 484 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
1171163impia 1258 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦))
118 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑏𝑦) = (𝑏𝑧))
119 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑧 → (𝑐𝑦) = (𝑐𝑧))
120118, 119eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑧 → ((𝑏𝑦) = (𝑐𝑦) ↔ (𝑏𝑧) = (𝑐𝑧)))
121120rspcv 3291 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → (𝑏𝑧) = (𝑐𝑧)))
122 breq2 4617 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
123122biimpd 219 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑧) = (𝑐𝑧) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧)))
124121, 123syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑤 → (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑎𝑧)𝑅(𝑐𝑧))))
125124com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) → ((𝑎𝑧)𝑅(𝑏𝑧) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧))))
126125imp 445 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
127126ad2ant2lr 783 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑧𝑤 → (𝑎𝑧)𝑅(𝑐𝑧)))
128127impcom 446 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
1291283adant1 1077 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑧)𝑅(𝑐𝑧))
130 raleq 3127 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦)))
131 fveq2 6148 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑎𝑡) = (𝑎𝑧))
132 fveq2 6148 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑧 → (𝑐𝑡) = (𝑐𝑧))
133131, 132breq12d 4626 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑧 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑧)𝑅(𝑐𝑧)))
134130, 133anbi12d 746 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑧 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))))
135134rspcev 3295 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
136104, 117, 129, 135syl12anc 1321 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
137136a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧𝑤 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1381373exp 1261 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
1392orderseqlem 31450 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝐹 → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
140139ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑎𝑧) ∈ (𝐴 ∪ {∅}))
1412orderseqlem 31450 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝐹 → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
142141ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑏𝑧) ∈ (𝐴 ∪ {∅}))
1432orderseqlem 31450 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐𝐹 → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
144143ad2antll 764 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (𝑐𝑧) ∈ (𝐴 ∪ {∅}))
145140, 142, 1443jca 1240 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅})))
146 potr 5007 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
1471, 145, 146sylancr 694 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) → (𝑎𝑧)𝑅(𝑐𝑧)))
148147impcom 446 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (𝑎𝑧)𝑅(𝑐𝑧))
149113, 148anim12i 589 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
150149anassrs 679 . . . . . . . . . . . . . . . . . 18 (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹))) → (∀𝑦𝑧 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑧)𝑅(𝑐𝑧)))
151150, 135sylan2 491 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ On ∧ ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ∧ ((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
152151exp32 630 . . . . . . . . . . . . . . . 16 (𝑧 ∈ On → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
153 raleq 3127 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
154153anbi2d 739 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑧 (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
155110, 154syl5bb 272 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
156 fveq2 6148 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑏𝑧) = (𝑏𝑤))
157 fveq2 6148 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝑐𝑧) = (𝑐𝑤))
158156, 157breq12d 4626 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((𝑏𝑧)𝑅(𝑐𝑧) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
159158anbi2d 739 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧)) ↔ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))))
160155, 159anbi12d 746 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → ((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) ↔ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))))
161160imbi1d 331 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (((∀𝑦𝑧 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑧)𝑅(𝑐𝑧))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))) ↔ (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
162152, 161syl5ibcom 235 . . . . . . . . . . . . . . 15 (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
163162adantr 481 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
164 simp1r 1084 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → 𝑤 ∈ On)
165 onelss 5725 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ On → (𝑤𝑧𝑤𝑧))
166165imp 445 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ On ∧ 𝑤𝑧) → 𝑤𝑧)
167166adantlr 750 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → 𝑤𝑧)
168 ssralv 3645 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦)))
169168anim1d 587 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦))))
170 r19.26 3057 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)))
171112ralimi 2947 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑤 ((𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
172170, 171sylbir 225 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑦𝑤 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
173169, 172syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑧 → ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
174173adantrd 484 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
175167, 174syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
1761753impia 1258 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦))
177 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑎𝑦) = (𝑎𝑤))
178 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑤 → (𝑏𝑦) = (𝑏𝑤))
179177, 178eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑤 → ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑎𝑤) = (𝑏𝑤)))
180179rspcv 3291 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑤) = (𝑏𝑤)))
181 breq1 4616 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑤) = (𝑏𝑤) → ((𝑎𝑤)𝑅(𝑐𝑤) ↔ (𝑏𝑤)𝑅(𝑐𝑤)))
182181biimprd 238 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑤) = (𝑏𝑤) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤)))
183180, 182syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑎𝑤)𝑅(𝑐𝑤))))
184183com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) → ((𝑏𝑤)𝑅(𝑐𝑤) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤))))
185184imp 445 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
186185ad2ant2rl 784 . . . . . . . . . . . . . . . . . . 19 (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (𝑤𝑧 → (𝑎𝑤)𝑅(𝑐𝑤)))
187186impcom 446 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
1881873adant1 1077 . . . . . . . . . . . . . . . . 17 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (𝑎𝑤)𝑅(𝑐𝑤))
189 raleq 3127 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ↔ ∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦)))
190 fveq2 6148 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑎𝑡) = (𝑎𝑤))
191 fveq2 6148 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑤 → (𝑐𝑡) = (𝑐𝑤))
192190, 191breq12d 4626 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑤 → ((𝑎𝑡)𝑅(𝑐𝑡) ↔ (𝑎𝑤)𝑅(𝑐𝑤)))
193189, 192anbi12d 746 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑤 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)) ↔ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))))
194193rspcev 3295 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ On ∧ (∀𝑦𝑤 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑤)𝑅(𝑐𝑤))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
195164, 176, 188, 194syl12anc 1321 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
196195a1d 25 . . . . . . . . . . . . . . 15 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤𝑧 ∧ ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
1971963exp 1261 . . . . . . . . . . . . . 14 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤𝑧 → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
198138, 163, 1973jaod 1389 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧𝑤𝑧 = 𝑤𝑤𝑧) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))))
199103, 198mpd 15 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
200199rexlimivv 3029 . . . . . . . . . . 11 (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ ∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦)) ∧ ((𝑎𝑧)𝑅(𝑏𝑧) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20199, 200sylbir 225 . . . . . . . . . 10 ((∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤))) → (((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
202201impcom 446 . . . . . . . . 9 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))
20394, 95, 202jca31 556 . . . . . . . 8 ((((𝑎𝐹𝑏𝐹) ∧ (𝑏𝐹𝑐𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
204203an4s 868 . . . . . . 7 ((((𝑎𝐹𝑏𝐹) ∧ ∃𝑧 ∈ On (∀𝑦𝑧 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑧)𝑅(𝑏𝑧))) ∧ ((𝑏𝐹𝑐𝐹) ∧ ∃𝑤 ∈ On (∀𝑦𝑤 (𝑏𝑦) = (𝑐𝑦) ∧ (𝑏𝑤)𝑅(𝑐𝑤)))) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
20564, 93, 204syl2anb 496 . . . . . 6 ((𝑎𝑆𝑏𝑏𝑆𝑐) → ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
206 raleq 3127 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦)))
207 fveq2 6148 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑓𝑥) = (𝑓𝑡))
208 fveq2 6148 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
209207, 208breq12d 4626 . . . . . . . . . . 11 (𝑥 = 𝑡 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑓𝑡)𝑅(𝑔𝑡)))
210206, 209anbi12d 746 . . . . . . . . . 10 (𝑥 = 𝑡 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡))))
211210cbvrexv 3160 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)))
21220ralbidv 2980 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦)))
213 fveq1 6147 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝑡) = (𝑎𝑡))
214213breq1d 4623 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑔𝑡)))
215212, 214anbi12d 746 . . . . . . . . . 10 (𝑓 = 𝑎 → ((∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
216215rexbidv 3045 . . . . . . . . 9 (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
217211, 216syl5bb 272 . . . . . . . 8 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))))
21818, 217anbi12d 746 . . . . . . 7 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)))))
21983anbi2d 739 . . . . . . . 8 (𝑔 = 𝑐 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑐𝐹)))
22085eqeq2d 2631 . . . . . . . . . . 11 (𝑔 = 𝑐 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑐𝑦)))
221220ralbidv 2980 . . . . . . . . . 10 (𝑔 = 𝑐 → (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦)))
222 fveq1 6147 . . . . . . . . . . 11 (𝑔 = 𝑐 → (𝑔𝑡) = (𝑐𝑡))
223222breq2d 4625 . . . . . . . . . 10 (𝑔 = 𝑐 → ((𝑎𝑡)𝑅(𝑔𝑡) ↔ (𝑎𝑡)𝑅(𝑐𝑡)))
224221, 223anbi12d 746 . . . . . . . . 9 (𝑔 = 𝑐 → ((∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
225224rexbidv 3045 . . . . . . . 8 (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
226219, 225anbi12d 746 . . . . . . 7 (𝑔 = 𝑐 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑡)𝑅(𝑔𝑡))) ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡)))))
22716, 65, 218, 226, 37brab 4958 . . . . . 6 (𝑎𝑆𝑐 ↔ ((𝑎𝐹𝑐𝐹) ∧ ∃𝑡 ∈ On (∀𝑦𝑡 (𝑎𝑦) = (𝑐𝑦) ∧ (𝑎𝑡)𝑅(𝑐𝑡))))
228205, 227sylibr 224 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)
22939, 228pm3.2i 471 . . . 4 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230229a1i 11 . . 3 ((𝑎𝐹𝑏𝐹𝑐𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231230rgen3 2970 . 2 𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232 df-po 4995 . 2 (𝑆 Po 𝐹 ↔ ∀𝑎𝐹𝑏𝐹𝑐𝐹𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233231, 232mpbir 221 1 𝑆 Po 𝐹
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3o 1035  w3a 1036   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  cun 3553  wss 3555  c0 3891  {csn 4148   class class class wbr 4613  {copab 4672   Po wpo 4993  Ord word 5681  Oncon0 5682  wf 5843  cfv 5847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-tr 4713  df-eprel 4985  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-ord 5685  df-on 5686  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855
This theorem is referenced by:  soseq  31452
  Copyright terms: Public domain W3C validator