Metamath Proof Explorer


Theorem poseq

Description: A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011)

Ref Expression
Hypotheses poseq.1 𝑅 Po ( 𝐴 ∪ { ∅ } )
poseq.2 𝐹 = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥𝐴 }
poseq.3 𝑆 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓𝐹𝑔𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) }
Assertion poseq 𝑆 Po 𝐹

Proof

Step Hyp Ref Expression
1 poseq.1 𝑅 Po ( 𝐴 ∪ { ∅ } )
2 poseq.2 𝐹 = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥𝐴 }
3 poseq.3 𝑆 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓𝐹𝑔𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) }
4 feq2 ( 𝑥 = 𝑏 → ( 𝑓 : 𝑥𝐴𝑓 : 𝑏𝐴 ) )
5 4 cbvrexvw ( ∃ 𝑥 ∈ On 𝑓 : 𝑥𝐴 ↔ ∃ 𝑏 ∈ On 𝑓 : 𝑏𝐴 )
6 5 abbii { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥𝐴 } = { 𝑓 ∣ ∃ 𝑏 ∈ On 𝑓 : 𝑏𝐴 }
7 2 6 eqtri 𝐹 = { 𝑓 ∣ ∃ 𝑏 ∈ On 𝑓 : 𝑏𝐴 }
8 7 orderseqlem ( 𝑎𝐹 → ( 𝑎𝑥 ) ∈ ( 𝐴 ∪ { ∅ } ) )
9 poirr ( ( 𝑅 Po ( 𝐴 ∪ { ∅ } ) ∧ ( 𝑎𝑥 ) ∈ ( 𝐴 ∪ { ∅ } ) ) → ¬ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) )
10 1 8 9 sylancr ( 𝑎𝐹 → ¬ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) )
11 10 intnand ( 𝑎𝐹 → ¬ ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) )
12 11 adantr ( ( 𝑎𝐹𝑥 ∈ On ) → ¬ ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) )
13 12 nrexdv ( 𝑎𝐹 → ¬ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) )
14 13 adantr ( ( 𝑎𝐹𝑎𝐹 ) → ¬ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) )
15 imnan ( ( ( 𝑎𝐹𝑎𝐹 ) → ¬ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) ) ↔ ¬ ( ( 𝑎𝐹𝑎𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) ) )
16 14 15 mpbi ¬ ( ( 𝑎𝐹𝑎𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) )
17 vex 𝑎 ∈ V
18 eleq1w ( 𝑓 = 𝑎 → ( 𝑓𝐹𝑎𝐹 ) )
19 18 anbi1d ( 𝑓 = 𝑎 → ( ( 𝑓𝐹𝑔𝐹 ) ↔ ( 𝑎𝐹𝑔𝐹 ) ) )
20 fveq1 ( 𝑓 = 𝑎 → ( 𝑓𝑦 ) = ( 𝑎𝑦 ) )
21 20 eqeq1d ( 𝑓 = 𝑎 → ( ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ) )
22 21 ralbidv ( 𝑓 = 𝑎 → ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ) )
23 fveq1 ( 𝑓 = 𝑎 → ( 𝑓𝑥 ) = ( 𝑎𝑥 ) )
24 23 breq1d ( 𝑓 = 𝑎 → ( ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ↔ ( 𝑎𝑥 ) 𝑅 ( 𝑔𝑥 ) ) )
25 22 24 anbi12d ( 𝑓 = 𝑎 → ( ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) )
26 25 rexbidv ( 𝑓 = 𝑎 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) )
27 19 26 anbi12d ( 𝑓 = 𝑎 → ( ( ( 𝑓𝐹𝑔𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) ↔ ( ( 𝑎𝐹𝑔𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) ) )
28 eleq1w ( 𝑔 = 𝑎 → ( 𝑔𝐹𝑎𝐹 ) )
29 28 anbi2d ( 𝑔 = 𝑎 → ( ( 𝑎𝐹𝑔𝐹 ) ↔ ( 𝑎𝐹𝑎𝐹 ) ) )
30 fveq1 ( 𝑔 = 𝑎 → ( 𝑔𝑦 ) = ( 𝑎𝑦 ) )
31 30 eqeq2d ( 𝑔 = 𝑎 → ( ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ↔ ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ) )
32 31 ralbidv ( 𝑔 = 𝑎 → ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ) )
33 fveq1 ( 𝑔 = 𝑎 → ( 𝑔𝑥 ) = ( 𝑎𝑥 ) )
34 33 breq2d ( 𝑔 = 𝑎 → ( ( 𝑎𝑥 ) 𝑅 ( 𝑔𝑥 ) ↔ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) )
35 32 34 anbi12d ( 𝑔 = 𝑎 → ( ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) ) )
36 35 rexbidv ( 𝑔 = 𝑎 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) ) )
37 29 36 anbi12d ( 𝑔 = 𝑎 → ( ( ( 𝑎𝐹𝑔𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) ↔ ( ( 𝑎𝐹𝑎𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) ) ) )
38 17 17 27 37 3 brab ( 𝑎 𝑆 𝑎 ↔ ( ( 𝑎𝐹𝑎𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑎𝑦 ) = ( 𝑎𝑦 ) ∧ ( 𝑎𝑥 ) 𝑅 ( 𝑎𝑥 ) ) ) )
39 16 38 mtbir ¬ 𝑎 𝑆 𝑎
40 vex 𝑏 ∈ V
41 raleq ( 𝑥 = 𝑧 → ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑧 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ) )
42 fveq2 ( 𝑥 = 𝑧 → ( 𝑓𝑥 ) = ( 𝑓𝑧 ) )
43 fveq2 ( 𝑥 = 𝑧 → ( 𝑔𝑥 ) = ( 𝑔𝑧 ) )
44 42 43 breq12d ( 𝑥 = 𝑧 → ( ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ↔ ( 𝑓𝑧 ) 𝑅 ( 𝑔𝑧 ) ) )
45 41 44 anbi12d ( 𝑥 = 𝑧 → ( ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ( ∀ 𝑦𝑧 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ) )
46 45 cbvrexvw ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑧 ) 𝑅 ( 𝑔𝑧 ) ) )
47 21 ralbidv ( 𝑓 = 𝑎 → ( ∀ 𝑦𝑧 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ) )
48 fveq1 ( 𝑓 = 𝑎 → ( 𝑓𝑧 ) = ( 𝑎𝑧 ) )
49 48 breq1d ( 𝑓 = 𝑎 → ( ( 𝑓𝑧 ) 𝑅 ( 𝑔𝑧 ) ↔ ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ) )
50 47 49 anbi12d ( 𝑓 = 𝑎 → ( ( ∀ 𝑦𝑧 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ↔ ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ) )
51 50 rexbidv ( 𝑓 = 𝑎 → ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ↔ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ) )
52 46 51 syl5bb ( 𝑓 = 𝑎 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ) )
53 19 52 anbi12d ( 𝑓 = 𝑎 → ( ( ( 𝑓𝐹𝑔𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) ↔ ( ( 𝑎𝐹𝑔𝐹 ) ∧ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ) ) )
54 eleq1w ( 𝑔 = 𝑏 → ( 𝑔𝐹𝑏𝐹 ) )
55 54 anbi2d ( 𝑔 = 𝑏 → ( ( 𝑎𝐹𝑔𝐹 ) ↔ ( 𝑎𝐹𝑏𝐹 ) ) )
56 fveq1 ( 𝑔 = 𝑏 → ( 𝑔𝑦 ) = ( 𝑏𝑦 ) )
57 56 eqeq2d ( 𝑔 = 𝑏 → ( ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ↔ ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ) )
58 57 ralbidv ( 𝑔 = 𝑏 → ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ) )
59 fveq1 ( 𝑔 = 𝑏 → ( 𝑔𝑧 ) = ( 𝑏𝑧 ) )
60 59 breq2d ( 𝑔 = 𝑏 → ( ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ↔ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) )
61 58 60 anbi12d ( 𝑔 = 𝑏 → ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ↔ ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ) )
62 61 rexbidv ( 𝑔 = 𝑏 → ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ↔ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ) )
63 55 62 anbi12d ( 𝑔 = 𝑏 → ( ( ( 𝑎𝐹𝑔𝐹 ) ∧ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑔𝑧 ) ) ) ↔ ( ( 𝑎𝐹𝑏𝐹 ) ∧ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ) ) )
64 17 40 53 63 3 brab ( 𝑎 𝑆 𝑏 ↔ ( ( 𝑎𝐹𝑏𝐹 ) ∧ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ) )
65 vex 𝑐 ∈ V
66 eleq1w ( 𝑓 = 𝑏 → ( 𝑓𝐹𝑏𝐹 ) )
67 66 anbi1d ( 𝑓 = 𝑏 → ( ( 𝑓𝐹𝑔𝐹 ) ↔ ( 𝑏𝐹𝑔𝐹 ) ) )
68 raleq ( 𝑥 = 𝑤 → ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑤 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ) )
69 fveq2 ( 𝑥 = 𝑤 → ( 𝑓𝑥 ) = ( 𝑓𝑤 ) )
70 fveq2 ( 𝑥 = 𝑤 → ( 𝑔𝑥 ) = ( 𝑔𝑤 ) )
71 69 70 breq12d ( 𝑥 = 𝑤 → ( ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ↔ ( 𝑓𝑤 ) 𝑅 ( 𝑔𝑤 ) ) )
72 68 71 anbi12d ( 𝑥 = 𝑤 → ( ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ( ∀ 𝑦𝑤 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ) )
73 72 cbvrexvw ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑤 ) 𝑅 ( 𝑔𝑤 ) ) )
74 fveq1 ( 𝑓 = 𝑏 → ( 𝑓𝑦 ) = ( 𝑏𝑦 ) )
75 74 eqeq1d ( 𝑓 = 𝑏 → ( ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ) )
76 75 ralbidv ( 𝑓 = 𝑏 → ( ∀ 𝑦𝑤 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ) )
77 fveq1 ( 𝑓 = 𝑏 → ( 𝑓𝑤 ) = ( 𝑏𝑤 ) )
78 77 breq1d ( 𝑓 = 𝑏 → ( ( 𝑓𝑤 ) 𝑅 ( 𝑔𝑤 ) ↔ ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ) )
79 76 78 anbi12d ( 𝑓 = 𝑏 → ( ( ∀ 𝑦𝑤 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ↔ ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ) )
80 79 rexbidv ( 𝑓 = 𝑏 → ( ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ↔ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ) )
81 73 80 syl5bb ( 𝑓 = 𝑏 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ) )
82 67 81 anbi12d ( 𝑓 = 𝑏 → ( ( ( 𝑓𝐹𝑔𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) ↔ ( ( 𝑏𝐹𝑔𝐹 ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ) ) )
83 eleq1w ( 𝑔 = 𝑐 → ( 𝑔𝐹𝑐𝐹 ) )
84 83 anbi2d ( 𝑔 = 𝑐 → ( ( 𝑏𝐹𝑔𝐹 ) ↔ ( 𝑏𝐹𝑐𝐹 ) ) )
85 fveq1 ( 𝑔 = 𝑐 → ( 𝑔𝑦 ) = ( 𝑐𝑦 ) )
86 85 eqeq2d ( 𝑔 = 𝑐 → ( ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ↔ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
87 86 ralbidv ( 𝑔 = 𝑐 → ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
88 fveq1 ( 𝑔 = 𝑐 → ( 𝑔𝑤 ) = ( 𝑐𝑤 ) )
89 88 breq2d ( 𝑔 = 𝑐 → ( ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ↔ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) )
90 87 89 anbi12d ( 𝑔 = 𝑐 → ( ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ↔ ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
91 90 rexbidv ( 𝑔 = 𝑐 → ( ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ↔ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
92 84 91 anbi12d ( 𝑔 = 𝑐 → ( ( ( 𝑏𝐹𝑔𝐹 ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑔𝑤 ) ) ) ↔ ( ( 𝑏𝐹𝑐𝐹 ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) )
93 40 65 82 92 3 brab ( 𝑏 𝑆 𝑐 ↔ ( ( 𝑏𝐹𝑐𝐹 ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
94 simplll ( ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) ∧ ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → 𝑎𝐹 )
95 simplrr ( ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) ∧ ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → 𝑐𝐹 )
96 an4 ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ↔ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
97 96 2rexbii ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ↔ ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
98 reeanv ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ↔ ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
99 97 98 bitri ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ↔ ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
100 eloni ( 𝑧 ∈ On → Ord 𝑧 )
101 eloni ( 𝑤 ∈ On → Ord 𝑤 )
102 ordtri3or ( ( Ord 𝑧 ∧ Ord 𝑤 ) → ( 𝑧𝑤𝑧 = 𝑤𝑤𝑧 ) )
103 100 101 102 syl2an ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧𝑤𝑧 = 𝑤𝑤𝑧 ) )
104 simp1l ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑧𝑤 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → 𝑧 ∈ On )
105 onelss ( 𝑤 ∈ On → ( 𝑧𝑤𝑧𝑤 ) )
106 105 imp ( ( 𝑤 ∈ On ∧ 𝑧𝑤 ) → 𝑧𝑤 )
107 106 adantll ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑧𝑤 ) → 𝑧𝑤 )
108 ssralv ( 𝑧𝑤 → ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) → ∀ 𝑦𝑧 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
109 108 anim2d ( 𝑧𝑤 → ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑧 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ) )
110 r19.26 ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ↔ ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑧 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
111 109 110 syl6ibr ( 𝑧𝑤 → ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ) )
112 eqtr ( ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ( 𝑎𝑦 ) = ( 𝑐𝑦 ) )
113 112 ralimi ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) )
114 111 113 syl6 ( 𝑧𝑤 → ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
115 107 114 syl ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑧𝑤 ) → ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
116 115 adantrd ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑧𝑤 ) → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
117 116 3impia ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑧𝑤 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) )
118 fveq2 ( 𝑦 = 𝑧 → ( 𝑏𝑦 ) = ( 𝑏𝑧 ) )
119 fveq2 ( 𝑦 = 𝑧 → ( 𝑐𝑦 ) = ( 𝑐𝑧 ) )
120 118 119 eqeq12d ( 𝑦 = 𝑧 → ( ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ↔ ( 𝑏𝑧 ) = ( 𝑐𝑧 ) ) )
121 120 rspcv ( 𝑧𝑤 → ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) → ( 𝑏𝑧 ) = ( 𝑐𝑧 ) ) )
122 breq2 ( ( 𝑏𝑧 ) = ( 𝑐𝑧 ) → ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ↔ ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
123 122 biimpd ( ( 𝑏𝑧 ) = ( 𝑐𝑧 ) → ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
124 121 123 syl6 ( 𝑧𝑤 → ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) → ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) )
125 124 com3l ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) → ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) → ( 𝑧𝑤 → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) )
126 125 imp ( ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) → ( 𝑧𝑤 → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
127 126 ad2ant2lr ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( 𝑧𝑤 → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
128 127 impcom ( ( 𝑧𝑤 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) )
129 128 3adant1 ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑧𝑤 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) )
130 raleq ( 𝑡 = 𝑧 → ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ↔ ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
131 fveq2 ( 𝑡 = 𝑧 → ( 𝑎𝑡 ) = ( 𝑎𝑧 ) )
132 fveq2 ( 𝑡 = 𝑧 → ( 𝑐𝑡 ) = ( 𝑐𝑧 ) )
133 131 132 breq12d ( 𝑡 = 𝑧 → ( ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ↔ ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
134 130 133 anbi12d ( 𝑡 = 𝑧 → ( ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ↔ ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) )
135 134 rspcev ( ( 𝑧 ∈ On ∧ ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) )
136 104 117 129 135 syl12anc ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑧𝑤 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) )
137 136 a1d ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑧𝑤 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
138 137 3exp ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧𝑤 → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) ) )
139 2 orderseqlem ( 𝑎𝐹 → ( 𝑎𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) )
140 139 ad2antrr ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ( 𝑎𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) )
141 2 orderseqlem ( 𝑏𝐹 → ( 𝑏𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) )
142 141 ad2antlr ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ( 𝑏𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) )
143 2 orderseqlem ( 𝑐𝐹 → ( 𝑐𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) )
144 143 ad2antll ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ( 𝑐𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) )
145 140 142 144 3jca ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ( ( 𝑎𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) ∧ ( 𝑏𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) ∧ ( 𝑐𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) ) )
146 potr ( ( 𝑅 Po ( 𝐴 ∪ { ∅ } ) ∧ ( ( 𝑎𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) ∧ ( 𝑏𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) ∧ ( 𝑐𝑧 ) ∈ ( 𝐴 ∪ { ∅ } ) ) ) → ( ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
147 1 145 146 sylancr ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ( ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
148 147 impcom ( ( ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ∧ ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) ) → ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) )
149 113 148 anim12i ( ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ∧ ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) ) ) → ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
150 149 anassrs ( ( ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) ∧ ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) ) → ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑐𝑧 ) ) )
151 150 135 sylan2 ( ( 𝑧 ∈ On ∧ ( ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) ∧ ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) )
152 151 exp32 ( 𝑧 ∈ On → ( ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) )
153 raleq ( 𝑧 = 𝑤 → ( ∀ 𝑦𝑧 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ↔ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
154 153 anbi2d ( 𝑧 = 𝑤 → ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑧 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ↔ ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ) )
155 110 154 syl5bb ( 𝑧 = 𝑤 → ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ↔ ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ) )
156 fveq2 ( 𝑧 = 𝑤 → ( 𝑏𝑧 ) = ( 𝑏𝑤 ) )
157 fveq2 ( 𝑧 = 𝑤 → ( 𝑐𝑧 ) = ( 𝑐𝑤 ) )
158 156 157 breq12d ( 𝑧 = 𝑤 → ( ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ↔ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) )
159 158 anbi2d ( 𝑧 = 𝑤 → ( ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ↔ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
160 155 159 anbi12d ( 𝑧 = 𝑤 → ( ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) ↔ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) )
161 160 imbi1d ( 𝑧 = 𝑤 → ( ( ( ∀ 𝑦𝑧 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑧 ) 𝑅 ( 𝑐𝑧 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) ↔ ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) ) )
162 152 161 syl5ibcom ( 𝑧 ∈ On → ( 𝑧 = 𝑤 → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) ) )
163 162 adantr ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧 = 𝑤 → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) ) )
164 simp1r ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑤𝑧 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → 𝑤 ∈ On )
165 onelss ( 𝑧 ∈ On → ( 𝑤𝑧𝑤𝑧 ) )
166 165 imp ( ( 𝑧 ∈ On ∧ 𝑤𝑧 ) → 𝑤𝑧 )
167 166 adantlr ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑤𝑧 ) → 𝑤𝑧 )
168 ssralv ( 𝑤𝑧 → ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) → ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ) )
169 168 anim1d ( 𝑤𝑧 → ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ( ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ) )
170 r19.26 ( ∀ 𝑦𝑤 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ↔ ( ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) )
171 112 ralimi ( ∀ 𝑦𝑤 ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) )
172 170 171 sylbir ( ( ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) )
173 169 172 syl6 ( 𝑤𝑧 → ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) → ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
174 173 adantrd ( 𝑤𝑧 → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
175 167 174 syl ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑤𝑧 ) → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
176 175 3impia ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑤𝑧 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) )
177 fveq2 ( 𝑦 = 𝑤 → ( 𝑎𝑦 ) = ( 𝑎𝑤 ) )
178 fveq2 ( 𝑦 = 𝑤 → ( 𝑏𝑦 ) = ( 𝑏𝑤 ) )
179 177 178 eqeq12d ( 𝑦 = 𝑤 → ( ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ↔ ( 𝑎𝑤 ) = ( 𝑏𝑤 ) ) )
180 179 rspcv ( 𝑤𝑧 → ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) → ( 𝑎𝑤 ) = ( 𝑏𝑤 ) ) )
181 breq1 ( ( 𝑎𝑤 ) = ( 𝑏𝑤 ) → ( ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ↔ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) )
182 181 biimprd ( ( 𝑎𝑤 ) = ( 𝑏𝑤 ) → ( ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) → ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ) )
183 180 182 syl6 ( 𝑤𝑧 → ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) → ( ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) → ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
184 183 com3l ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) → ( ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) → ( 𝑤𝑧 → ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
185 184 imp ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) → ( 𝑤𝑧 → ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ) )
186 185 ad2ant2rl ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( 𝑤𝑧 → ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ) )
187 186 impcom ( ( 𝑤𝑧 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) )
188 187 3adant1 ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑤𝑧 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) )
189 raleq ( 𝑡 = 𝑤 → ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ↔ ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
190 fveq2 ( 𝑡 = 𝑤 → ( 𝑎𝑡 ) = ( 𝑎𝑤 ) )
191 fveq2 ( 𝑡 = 𝑤 → ( 𝑐𝑡 ) = ( 𝑐𝑤 ) )
192 190 191 breq12d ( 𝑡 = 𝑤 → ( ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ↔ ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ) )
193 189 192 anbi12d ( 𝑡 = 𝑤 → ( ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ↔ ( ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) )
194 193 rspcev ( ( 𝑤 ∈ On ∧ ( ∀ 𝑦𝑤 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) )
195 164 176 188 194 syl12anc ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑤𝑧 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) )
196 195 a1d ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ 𝑤𝑧 ∧ ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
197 196 3exp ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑤𝑧 → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) ) )
198 138 163 197 3jaod ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( ( 𝑧𝑤𝑧 = 𝑤𝑤𝑧 ) → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) ) )
199 103 198 mpd ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) )
200 199 rexlimivv ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ) ∧ ( ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
201 99 200 sylbir ( ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) → ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
202 201 impcom ( ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) ∧ ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) )
203 94 95 202 jca31 ( ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ( 𝑏𝐹𝑐𝐹 ) ) ∧ ( ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ( ( 𝑎𝐹𝑐𝐹 ) ∧ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
204 203 an4s ( ( ( ( 𝑎𝐹𝑏𝐹 ) ∧ ∃ 𝑧 ∈ On ( ∀ 𝑦𝑧 ( 𝑎𝑦 ) = ( 𝑏𝑦 ) ∧ ( 𝑎𝑧 ) 𝑅 ( 𝑏𝑧 ) ) ) ∧ ( ( 𝑏𝐹𝑐𝐹 ) ∧ ∃ 𝑤 ∈ On ( ∀ 𝑦𝑤 ( 𝑏𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑏𝑤 ) 𝑅 ( 𝑐𝑤 ) ) ) ) → ( ( 𝑎𝐹𝑐𝐹 ) ∧ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
205 64 93 204 syl2anb ( ( 𝑎 𝑆 𝑏𝑏 𝑆 𝑐 ) → ( ( 𝑎𝐹𝑐𝐹 ) ∧ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
206 raleq ( 𝑥 = 𝑡 → ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑡 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ) )
207 fveq2 ( 𝑥 = 𝑡 → ( 𝑓𝑥 ) = ( 𝑓𝑡 ) )
208 fveq2 ( 𝑥 = 𝑡 → ( 𝑔𝑥 ) = ( 𝑔𝑡 ) )
209 207 208 breq12d ( 𝑥 = 𝑡 → ( ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ↔ ( 𝑓𝑡 ) 𝑅 ( 𝑔𝑡 ) ) )
210 206 209 anbi12d ( 𝑥 = 𝑡 → ( ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ( ∀ 𝑦𝑡 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ) )
211 210 cbvrexvw ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑡 ) 𝑅 ( 𝑔𝑡 ) ) )
212 21 ralbidv ( 𝑓 = 𝑎 → ( ∀ 𝑦𝑡 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ) )
213 fveq1 ( 𝑓 = 𝑎 → ( 𝑓𝑡 ) = ( 𝑎𝑡 ) )
214 213 breq1d ( 𝑓 = 𝑎 → ( ( 𝑓𝑡 ) 𝑅 ( 𝑔𝑡 ) ↔ ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ) )
215 212 214 anbi12d ( 𝑓 = 𝑎 → ( ( ∀ 𝑦𝑡 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ↔ ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ) )
216 215 rexbidv ( 𝑓 = 𝑎 → ( ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ↔ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ) )
217 211 216 syl5bb ( 𝑓 = 𝑎 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ↔ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ) )
218 19 217 anbi12d ( 𝑓 = 𝑎 → ( ( ( 𝑓𝐹𝑔𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) ) ↔ ( ( 𝑎𝐹𝑔𝐹 ) ∧ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ) ) )
219 83 anbi2d ( 𝑔 = 𝑐 → ( ( 𝑎𝐹𝑔𝐹 ) ↔ ( 𝑎𝐹𝑐𝐹 ) ) )
220 85 eqeq2d ( 𝑔 = 𝑐 → ( ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ↔ ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
221 220 ralbidv ( 𝑔 = 𝑐 → ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ↔ ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ) )
222 fveq1 ( 𝑔 = 𝑐 → ( 𝑔𝑡 ) = ( 𝑐𝑡 ) )
223 222 breq2d ( 𝑔 = 𝑐 → ( ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ↔ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) )
224 221 223 anbi12d ( 𝑔 = 𝑐 → ( ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ↔ ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
225 224 rexbidv ( 𝑔 = 𝑐 → ( ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ↔ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
226 219 225 anbi12d ( 𝑔 = 𝑐 → ( ( ( 𝑎𝐹𝑔𝐹 ) ∧ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑔𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑔𝑡 ) ) ) ↔ ( ( 𝑎𝐹𝑐𝐹 ) ∧ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) ) )
227 17 65 218 226 3 brab ( 𝑎 𝑆 𝑐 ↔ ( ( 𝑎𝐹𝑐𝐹 ) ∧ ∃ 𝑡 ∈ On ( ∀ 𝑦𝑡 ( 𝑎𝑦 ) = ( 𝑐𝑦 ) ∧ ( 𝑎𝑡 ) 𝑅 ( 𝑐𝑡 ) ) ) )
228 205 227 sylibr ( ( 𝑎 𝑆 𝑏𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 )
229 39 228 pm3.2i ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) )
230 229 a1i ( ( 𝑎𝐹𝑏𝐹𝑐𝐹 ) → ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) )
231 230 rgen3 𝑎𝐹𝑏𝐹𝑐𝐹 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) )
232 df-po ( 𝑆 Po 𝐹 ↔ ∀ 𝑎𝐹𝑏𝐹𝑐𝐹 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) )
233 231 232 mpbir 𝑆 Po 𝐹