Metamath Proof Explorer

Theorem poseq

Description: A partial ordering of ordinal sequences. (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 bitrid ⊢ ( 𝑓 = 𝑎 → ( ∃ 𝑥 ∈ 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 bitrid ⊢ ( 𝑓 = 𝑏 → ( ∃ 𝑥 ∈ 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 imbitrrdi ⊢ ( 𝑧 ⊆ 𝑤 → ( ( ∀ 𝑦 ∈ 𝑧 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝑧 ( ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) ) )
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 bitrid ⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑦 ∈ 𝑧 ( ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝑧 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑏 ‘ 𝑦 ) = ( 𝑐 ‘ 𝑦 ) ) ) )
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 bitrid ⊢ ( 𝑓 = 𝑎 → ( ∃ 𝑥 ∈ 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 𝐹