Metamath Proof Explorer

Theorem soseq

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

Ref Expression
Hypotheses soseq.1 ⊢ 𝑅 Or ( 𝐴 ∪ { ∅ } )
soseq.2 ⊢ 𝐹 = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 }
soseq.3 ⊢ 𝑆 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) }
soseq.4 ⊢ ¬ ∅ ∈ 𝐴
Assertion soseq 𝑆 Or 𝐹

Proof

Step Hyp Ref Expression
1 soseq.1 ⊢ 𝑅 Or ( 𝐴 ∪ { ∅ } )
2 soseq.2 ⊢ 𝐹 = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 }
3 soseq.3 ⊢ 𝑆 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) }
4 soseq.4 ⊢ ¬ ∅ ∈ 𝐴
5 sopo ⊢ ( 𝑅 Or ( 𝐴 ∪ { ∅ } ) → 𝑅 Po ( 𝐴 ∪ { ∅ } ) )
6 1 5 ax-mp ⊢ 𝑅 Po ( 𝐴 ∪ { ∅ } )
7 6 2 3 poseq ⊢ 𝑆 Po 𝐹
8 eleq1w ⊢ ( 𝑓 = 𝑎 → ( 𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹 ) )
9 8 anbi1d ⊢ ( 𝑓 = 𝑎 → ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ↔ ( 𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ) )
10 fveq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) )
11 10 eqeq1d ⊢ ( 𝑓 = 𝑎 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) )
12 11 ralbidv ⊢ ( 𝑓 = 𝑎 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) )
13 fveq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑥 ) )
14 13 breq1d ⊢ ( 𝑓 = 𝑎 → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) )
15 12 14 anbi12d ⊢ ( 𝑓 = 𝑎 → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
16 15 rexbidv ⊢ ( 𝑓 = 𝑎 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
17 9 16 anbi12d ⊢ ( 𝑓 = 𝑎 → ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( ( 𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) )
18 eleq1w ⊢ ( 𝑔 = 𝑏 → ( 𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹 ) )
19 18 anbi2d ⊢ ( 𝑔 = 𝑏 → ( ( 𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ↔ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) ) )
20 fveq1 ⊢ ( 𝑔 = 𝑏 → ( 𝑔 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
21 20 eqeq2d ⊢ ( 𝑔 = 𝑏 → ( ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ) )
22 21 ralbidv ⊢ ( 𝑔 = 𝑏 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ) )
23 fveq1 ⊢ ( 𝑔 = 𝑏 → ( 𝑔 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
24 23 breq2d ⊢ ( 𝑔 = 𝑏 → ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) )
25 22 24 anbi12d ⊢ ( 𝑔 = 𝑏 → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ) )
26 25 rexbidv ⊢ ( 𝑔 = 𝑏 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ) )
27 19 26 anbi12d ⊢ ( 𝑔 = 𝑏 → ( ( ( 𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ) ) )
28 17 27 3 brabg ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( 𝑎 𝑆 𝑏 ↔ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ) ) )
29 28 bianabs ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( 𝑎 𝑆 𝑏 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ) )
30 eleq1w ⊢ ( 𝑓 = 𝑏 → ( 𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹 ) )
31 30 anbi1d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ↔ ( 𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ) )
32 fveq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
33 32 eqeq1d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) )
34 33 ralbidv ⊢ ( 𝑓 = 𝑏 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) )
35 fveq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
36 35 breq1d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) )
37 34 36 anbi12d ⊢ ( 𝑓 = 𝑏 → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
38 37 rexbidv ⊢ ( 𝑓 = 𝑏 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
39 31 38 anbi12d ⊢ ( 𝑓 = 𝑏 → ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( ( 𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) )
40 eleq1w ⊢ ( 𝑔 = 𝑎 → ( 𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹 ) )
41 40 anbi2d ⊢ ( 𝑔 = 𝑎 → ( ( 𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ↔ ( 𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) ) )
42 fveq1 ⊢ ( 𝑔 = 𝑎 → ( 𝑔 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) )
43 42 eqeq2d ⊢ ( 𝑔 = 𝑎 → ( ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ) )
44 43 ralbidv ⊢ ( 𝑔 = 𝑎 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ) )
45 fveq1 ⊢ ( 𝑔 = 𝑎 → ( 𝑔 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑥 ) )
46 45 breq2d ⊢ ( 𝑔 = 𝑎 → ( ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) )
47 44 46 anbi12d ⊢ ( 𝑔 = 𝑎 → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
48 47 rexbidv ⊢ ( 𝑔 = 𝑎 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
49 41 48 anbi12d ⊢ ( 𝑔 = 𝑎 → ( ( ( 𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( ( 𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ) )
50 39 49 3 brabg ⊢ ( ( 𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) → ( 𝑏 𝑆 𝑎 ↔ ( ( 𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ) )
51 50 bianabs ⊢ ( ( 𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) → ( 𝑏 𝑆 𝑎 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
52 51 ancoms ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( 𝑏 𝑆 𝑎 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
53 29 52 orbi12d ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ( 𝑎 𝑆 𝑏 ∨ 𝑏 𝑆 𝑎 ) ↔ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ) )
54 53 notbid ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ¬ ( 𝑎 𝑆 𝑏 ∨ 𝑏 𝑆 𝑎 ) ↔ ¬ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ) )
55 ralinexa ⊢ ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ¬ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ↔ ¬ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
56 andi ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ↔ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
57 eqcom ⊢ ( ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) )
58 57 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) )
59 58 anbi1i ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) )
60 59 orbi2i ⊢ ( ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ↔ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
61 56 60 bitri ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ↔ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
62 61 rexbii ⊢ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ On ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
63 r19.43 ⊢ ( ∃ 𝑥 ∈ On ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ↔ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
64 62 63 bitri ⊢ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ↔ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
65 55 64 xchbinx ⊢ ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ¬ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ↔ ¬ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
66 feq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑓 : 𝑥 ⟶ 𝐴 ↔ 𝑓 : 𝑦 ⟶ 𝐴 ) )
67 66 cbvrexvw ⊢ ( ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 ↔ ∃ 𝑦 ∈ On 𝑓 : 𝑦 ⟶ 𝐴 )
68 67 abbii ⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 } = { 𝑓 ∣ ∃ 𝑦 ∈ On 𝑓 : 𝑦 ⟶ 𝐴 }
69 2 68 eqtri ⊢ 𝐹 = { 𝑓 ∣ ∃ 𝑦 ∈ On 𝑓 : 𝑦 ⟶ 𝐴 }
70 69 orderseqlem ⊢ ( 𝑎 ∈ 𝐹 → ( 𝑎 ‘ 𝑥 ) ∈ ( 𝐴 ∪ { ∅ } ) )
71 69 orderseqlem ⊢ ( 𝑏 ∈ 𝐹 → ( 𝑏 ‘ 𝑥 ) ∈ ( 𝐴 ∪ { ∅ } ) )
72 sotrieq ⊢ ( ( 𝑅 Or ( 𝐴 ∪ { ∅ } ) ∧ ( ( 𝑎 ‘ 𝑥 ) ∈ ( 𝐴 ∪ { ∅ } ) ∧ ( 𝑏 ‘ 𝑥 ) ∈ ( 𝐴 ∪ { ∅ } ) ) ) → ( ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ¬ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
73 1 72 mpan ⊢ ( ( ( 𝑎 ‘ 𝑥 ) ∈ ( 𝐴 ∪ { ∅ } ) ∧ ( 𝑏 ‘ 𝑥 ) ∈ ( 𝐴 ∪ { ∅ } ) ) → ( ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ¬ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
74 70 71 73 syl2an ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ¬ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) )
75 74 imbi2d ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ¬ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ) )
76 75 ralbidv ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ¬ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) ) )
77 vex ⊢ 𝑦 ∈ V
78 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑦 ) )
79 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑏 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑦 ) )
80 78 79 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ) )
81 77 80 sbcie ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
82 81 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
83 82 imbi1i ⊢ ( ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
84 83 ralbii ⊢ ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
85 tfisg ⊢ ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
86 84 85 sylbir ⊢ ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
87 vex ⊢ 𝑎 ∈ V
88 feq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 : 𝑥 ⟶ 𝐴 ↔ 𝑎 : 𝑥 ⟶ 𝐴 ) )
89 88 rexbidv ⊢ ( 𝑓 = 𝑎 → ( ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 ↔ ∃ 𝑥 ∈ On 𝑎 : 𝑥 ⟶ 𝐴 ) )
90 87 89 2 elab2 ⊢ ( 𝑎 ∈ 𝐹 ↔ ∃ 𝑥 ∈ On 𝑎 : 𝑥 ⟶ 𝐴 )
91 feq2 ⊢ ( 𝑥 = 𝑝 → ( 𝑎 : 𝑥 ⟶ 𝐴 ↔ 𝑎 : 𝑝 ⟶ 𝐴 ) )
92 91 cbvrexvw ⊢ ( ∃ 𝑥 ∈ On 𝑎 : 𝑥 ⟶ 𝐴 ↔ ∃ 𝑝 ∈ On 𝑎 : 𝑝 ⟶ 𝐴 )
93 90 92 bitri ⊢ ( 𝑎 ∈ 𝐹 ↔ ∃ 𝑝 ∈ On 𝑎 : 𝑝 ⟶ 𝐴 )
94 vex ⊢ 𝑏 ∈ V
95 feq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 : 𝑥 ⟶ 𝐴 ↔ 𝑏 : 𝑥 ⟶ 𝐴 ) )
96 95 rexbidv ⊢ ( 𝑓 = 𝑏 → ( ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 ↔ ∃ 𝑥 ∈ On 𝑏 : 𝑥 ⟶ 𝐴 ) )
97 94 96 2 elab2 ⊢ ( 𝑏 ∈ 𝐹 ↔ ∃ 𝑥 ∈ On 𝑏 : 𝑥 ⟶ 𝐴 )
98 feq2 ⊢ ( 𝑥 = 𝑞 → ( 𝑏 : 𝑥 ⟶ 𝐴 ↔ 𝑏 : 𝑞 ⟶ 𝐴 ) )
99 98 cbvrexvw ⊢ ( ∃ 𝑥 ∈ On 𝑏 : 𝑥 ⟶ 𝐴 ↔ ∃ 𝑞 ∈ On 𝑏 : 𝑞 ⟶ 𝐴 )
100 97 99 bitri ⊢ ( 𝑏 ∈ 𝐹 ↔ ∃ 𝑞 ∈ On 𝑏 : 𝑞 ⟶ 𝐴 )
101 93 100 anbi12i ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) ↔ ( ∃ 𝑝 ∈ On 𝑎 : 𝑝 ⟶ 𝐴 ∧ ∃ 𝑞 ∈ On 𝑏 : 𝑞 ⟶ 𝐴 ) )
102 reeanv ⊢ ( ∃ 𝑝 ∈ On ∃ 𝑞 ∈ On ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ↔ ( ∃ 𝑝 ∈ On 𝑎 : 𝑝 ⟶ 𝐴 ∧ ∃ 𝑞 ∈ On 𝑏 : 𝑞 ⟶ 𝐴 ) )
103 101 102 bitr4i ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) ↔ ∃ 𝑝 ∈ On ∃ 𝑞 ∈ On ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) )
104 onss ⊢ ( 𝑞 ∈ On → 𝑞 ⊆ On )
105 ssralv ⊢ ( 𝑞 ⊆ On → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
106 104 105 syl ⊢ ( 𝑞 ∈ On → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
107 106 ad2antlr ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
108 fveq2 ⊢ ( 𝑥 = 𝑝 → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑝 ) )
109 fveq2 ⊢ ( 𝑥 = 𝑝 → ( 𝑏 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑝 ) )
110 108 109 eqeq12d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) ) )
111 110 rspcv ⊢ ( 𝑝 ∈ 𝑞 → ( ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) ) )
112 111 a1i ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( 𝑝 ∈ 𝑞 → ( ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) ) ) )
113 ffvelcdm ⊢ ( ( 𝑏 : 𝑞 ⟶ 𝐴 ∧ 𝑝 ∈ 𝑞 ) → ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 )
114 fdm ⊢ ( 𝑎 : 𝑝 ⟶ 𝐴 → dom 𝑎 = 𝑝 )
115 eloni ⊢ ( 𝑝 ∈ On → Ord 𝑝 )
116 ordirr ⊢ ( Ord 𝑝 → ¬ 𝑝 ∈ 𝑝 )
117 115 116 syl ⊢ ( 𝑝 ∈ On → ¬ 𝑝 ∈ 𝑝 )
118 eleq2 ⊢ ( dom 𝑎 = 𝑝 → ( 𝑝 ∈ dom 𝑎 ↔ 𝑝 ∈ 𝑝 ) )
119 118 notbid ⊢ ( dom 𝑎 = 𝑝 → ( ¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝 ∈ 𝑝 ) )
120 119 biimparc ⊢ ( ( ¬ 𝑝 ∈ 𝑝 ∧ dom 𝑎 = 𝑝 ) → ¬ 𝑝 ∈ dom 𝑎 )
121 117 120 sylan ⊢ ( ( 𝑝 ∈ On ∧ dom 𝑎 = 𝑝 ) → ¬ 𝑝 ∈ dom 𝑎 )
122 ndmfv ⊢ ( ¬ 𝑝 ∈ dom 𝑎 → ( 𝑎 ‘ 𝑝 ) = ∅ )
123 eqtr2 ⊢ ( ( ( 𝑎 ‘ 𝑝 ) = ∅ ∧ ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) ) → ∅ = ( 𝑏 ‘ 𝑝 ) )
124 eleq1 ⊢ ( ∅ = ( 𝑏 ‘ 𝑝 ) → ( ∅ ∈ 𝐴 ↔ ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 ) )
125 124 biimprd ⊢ ( ∅ = ( 𝑏 ‘ 𝑝 ) → ( ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 → ∅ ∈ 𝐴 ) )
126 123 125 syl ⊢ ( ( ( 𝑎 ‘ 𝑝 ) = ∅ ∧ ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) ) → ( ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 → ∅ ∈ 𝐴 ) )
127 126 ex ⊢ ( ( 𝑎 ‘ 𝑝 ) = ∅ → ( ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) → ( ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 → ∅ ∈ 𝐴 ) ) )
128 121 122 127 3syl ⊢ ( ( 𝑝 ∈ On ∧ dom 𝑎 = 𝑝 ) → ( ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) → ( ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 → ∅ ∈ 𝐴 ) ) )
129 128 com23 ⊢ ( ( 𝑝 ∈ On ∧ dom 𝑎 = 𝑝 ) → ( ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 → ( ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) → ∅ ∈ 𝐴 ) ) )
130 114 129 sylan2 ⊢ ( ( 𝑝 ∈ On ∧ 𝑎 : 𝑝 ⟶ 𝐴 ) → ( ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 → ( ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) → ∅ ∈ 𝐴 ) ) )
131 130 adantlr ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ 𝑎 : 𝑝 ⟶ 𝐴 ) → ( ( 𝑏 ‘ 𝑝 ) ∈ 𝐴 → ( ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) → ∅ ∈ 𝐴 ) ) )
132 113 131 syl5 ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ 𝑎 : 𝑝 ⟶ 𝐴 ) → ( ( 𝑏 : 𝑞 ⟶ 𝐴 ∧ 𝑝 ∈ 𝑞 ) → ( ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) → ∅ ∈ 𝐴 ) ) )
133 132 exp4b ⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( 𝑎 : 𝑝 ⟶ 𝐴 → ( 𝑏 : 𝑞 ⟶ 𝐴 → ( 𝑝 ∈ 𝑞 → ( ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) → ∅ ∈ 𝐴 ) ) ) ) )
134 133 imp32 ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( 𝑝 ∈ 𝑞 → ( ( 𝑎 ‘ 𝑝 ) = ( 𝑏 ‘ 𝑝 ) → ∅ ∈ 𝐴 ) ) )
135 112 134 syldd ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( 𝑝 ∈ 𝑞 → ( ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ∅ ∈ 𝐴 ) ) )
136 135 com23 ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑝 ∈ 𝑞 → ∅ ∈ 𝐴 ) ) )
137 136 imp ⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) → ( 𝑝 ∈ 𝑞 → ∅ ∈ 𝐴 ) )
138 4 137 mtoi ⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) → ¬ 𝑝 ∈ 𝑞 )
139 138 ex ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝑞 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ¬ 𝑝 ∈ 𝑞 ) )
140 107 139 syld ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ¬ 𝑝 ∈ 𝑞 ) )
141 onss ⊢ ( 𝑝 ∈ On → 𝑝 ⊆ On )
142 ssralv ⊢ ( 𝑝 ⊆ On → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
143 141 142 syl ⊢ ( 𝑝 ∈ On → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
144 143 ad2antrr ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
145 fveq2 ⊢ ( 𝑥 = 𝑞 → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑞 ) )
146 fveq2 ⊢ ( 𝑥 = 𝑞 → ( 𝑏 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑞 ) )
147 145 146 eqeq12d ⊢ ( 𝑥 = 𝑞 → ( ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) ) )
148 147 rspcv ⊢ ( 𝑞 ∈ 𝑝 → ( ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) ) )
149 148 a1i ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( 𝑞 ∈ 𝑝 → ( ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) ) ) )
150 ffvelcdm ⊢ ( ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑞 ∈ 𝑝 ) → ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 )
151 fdm ⊢ ( 𝑏 : 𝑞 ⟶ 𝐴 → dom 𝑏 = 𝑞 )
152 eloni ⊢ ( 𝑞 ∈ On → Ord 𝑞 )
153 ordirr ⊢ ( Ord 𝑞 → ¬ 𝑞 ∈ 𝑞 )
154 152 153 syl ⊢ ( 𝑞 ∈ On → ¬ 𝑞 ∈ 𝑞 )
155 eleq2 ⊢ ( dom 𝑏 = 𝑞 → ( 𝑞 ∈ dom 𝑏 ↔ 𝑞 ∈ 𝑞 ) )
156 155 notbid ⊢ ( dom 𝑏 = 𝑞 → ( ¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞 ∈ 𝑞 ) )
157 156 biimparc ⊢ ( ( ¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞 ) → ¬ 𝑞 ∈ dom 𝑏 )
158 ndmfv ⊢ ( ¬ 𝑞 ∈ dom 𝑏 → ( 𝑏 ‘ 𝑞 ) = ∅ )
159 157 158 syl ⊢ ( ( ¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞 ) → ( 𝑏 ‘ 𝑞 ) = ∅ )
160 154 159 sylan ⊢ ( ( 𝑞 ∈ On ∧ dom 𝑏 = 𝑞 ) → ( 𝑏 ‘ 𝑞 ) = ∅ )
161 eqtr ⊢ ( ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) ∧ ( 𝑏 ‘ 𝑞 ) = ∅ ) → ( 𝑎 ‘ 𝑞 ) = ∅ )
162 eleq1 ⊢ ( ( 𝑎 ‘ 𝑞 ) = ∅ → ( ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) )
163 162 biimpd ⊢ ( ( 𝑎 ‘ 𝑞 ) = ∅ → ( ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 → ∅ ∈ 𝐴 ) )
164 161 163 syl ⊢ ( ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) ∧ ( 𝑏 ‘ 𝑞 ) = ∅ ) → ( ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 → ∅ ∈ 𝐴 ) )
165 164 expcom ⊢ ( ( 𝑏 ‘ 𝑞 ) = ∅ → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ( ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 → ∅ ∈ 𝐴 ) ) )
166 165 com23 ⊢ ( ( 𝑏 ‘ 𝑞 ) = ∅ → ( ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ∅ ∈ 𝐴 ) ) )
167 160 166 syl ⊢ ( ( 𝑞 ∈ On ∧ dom 𝑏 = 𝑞 ) → ( ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ∅ ∈ 𝐴 ) ) )
168 167 adantll ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ dom 𝑏 = 𝑞 ) → ( ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ∅ ∈ 𝐴 ) ) )
169 151 168 sylan2 ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) → ( ( 𝑎 ‘ 𝑞 ) ∈ 𝐴 → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ∅ ∈ 𝐴 ) ) )
170 150 169 syl5 ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) → ( ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑞 ∈ 𝑝 ) → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ∅ ∈ 𝐴 ) ) )
171 170 exp4b ⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( 𝑏 : 𝑞 ⟶ 𝐴 → ( 𝑎 : 𝑝 ⟶ 𝐴 → ( 𝑞 ∈ 𝑝 → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ∅ ∈ 𝐴 ) ) ) ) )
172 171 com23 ⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( 𝑎 : 𝑝 ⟶ 𝐴 → ( 𝑏 : 𝑞 ⟶ 𝐴 → ( 𝑞 ∈ 𝑝 → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ∅ ∈ 𝐴 ) ) ) ) )
173 172 imp32 ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( 𝑞 ∈ 𝑝 → ( ( 𝑎 ‘ 𝑞 ) = ( 𝑏 ‘ 𝑞 ) → ∅ ∈ 𝐴 ) ) )
174 149 173 syldd ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( 𝑞 ∈ 𝑝 → ( ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ∅ ∈ 𝐴 ) ) )
175 174 com23 ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑞 ∈ 𝑝 → ∅ ∈ 𝐴 ) ) )
176 175 imp ⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) → ( 𝑞 ∈ 𝑝 → ∅ ∈ 𝐴 ) )
177 4 176 mtoi ⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) → ¬ 𝑞 ∈ 𝑝 )
178 177 ex ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ¬ 𝑞 ∈ 𝑝 ) )
179 144 178 syld ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ¬ 𝑞 ∈ 𝑝 ) )
180 140 179 jcad ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( ¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝 ) ) )
181 ordtri3or ⊢ ( ( Ord 𝑝 ∧ Ord 𝑞 ) → ( 𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝 ) )
182 115 152 181 syl2an ⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( 𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝 ) )
183 182 adantr ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( 𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝 ) )
184 3orel13 ⊢ ( ( ¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝 ) → ( ( 𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝 ) → 𝑝 = 𝑞 ) )
185 180 183 184 syl6ci ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → 𝑝 = 𝑞 ) )
186 185 144 jcad ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → ( 𝑝 = 𝑞 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) )
187 ffn ⊢ ( 𝑎 : 𝑝 ⟶ 𝐴 → 𝑎 Fn 𝑝 )
188 ffn ⊢ ( 𝑏 : 𝑞 ⟶ 𝐴 → 𝑏 Fn 𝑞 )
189 eqfnfv2 ⊢ ( ( 𝑎 Fn 𝑝 ∧ 𝑏 Fn 𝑞 ) → ( 𝑎 = 𝑏 ↔ ( 𝑝 = 𝑞 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) )
190 187 188 189 syl2an ⊢ ( ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) → ( 𝑎 = 𝑏 ↔ ( 𝑝 = 𝑞 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) )
191 190 adantl ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( 𝑎 = 𝑏 ↔ ( 𝑝 = 𝑞 ∧ ∀ 𝑥 ∈ 𝑝 ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) )
192 186 191 sylibrd ⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → 𝑎 = 𝑏 ) )
193 192 ex ⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → 𝑎 = 𝑏 ) ) )
194 193 rexlimivv ⊢ ( ∃ 𝑝 ∈ On ∃ 𝑞 ∈ On ( 𝑎 : 𝑝 ⟶ 𝐴 ∧ 𝑏 : 𝑞 ⟶ 𝐴 ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → 𝑎 = 𝑏 ) )
195 103 194 sylbi ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ On ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) → 𝑎 = 𝑏 ) )
196 86 195 syl5 ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) → 𝑎 = 𝑏 ) )
197 76 196 sylbird ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) → ¬ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ∨ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) → 𝑎 = 𝑏 ) )
198 65 197 biimtrrid ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ¬ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑎 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) ∧ ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ∨ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑏 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑦 ) ∧ ( 𝑏 ‘ 𝑥 ) 𝑅 ( 𝑎 ‘ 𝑥 ) ) ) → 𝑎 = 𝑏 ) )
199 54 198 sylbid ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ¬ ( 𝑎 𝑆 𝑏 ∨ 𝑏 𝑆 𝑎 ) → 𝑎 = 𝑏 ) )
200 199 orrd ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ( 𝑎 𝑆 𝑏 ∨ 𝑏 𝑆 𝑎 ) ∨ 𝑎 = 𝑏 ) )
201 3orcomb ⊢ ( ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) ↔ ( 𝑎 𝑆 𝑏 ∨ 𝑏 𝑆 𝑎 ∨ 𝑎 = 𝑏 ) )
202 df-3or ⊢ ( ( 𝑎 𝑆 𝑏 ∨ 𝑏 𝑆 𝑎 ∨ 𝑎 = 𝑏 ) ↔ ( ( 𝑎 𝑆 𝑏 ∨ 𝑏 𝑆 𝑎 ) ∨ 𝑎 = 𝑏 ) )
203 201 202 bitr2i ⊢ ( ( ( 𝑎 𝑆 𝑏 ∨ 𝑏 𝑆 𝑎 ) ∨ 𝑎 = 𝑏 ) ↔ ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) )
204 200 203 sylib ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) )
205 204 rgen2 ⊢ ∀ 𝑎 ∈ 𝐹 ∀ 𝑏 ∈ 𝐹 ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 )
206 df-so ⊢ ( 𝑆 Or 𝐹 ↔ ( 𝑆 Po 𝐹 ∧ ∀ 𝑎 ∈ 𝐹 ∀ 𝑏 ∈ 𝐹 ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) ) )
207 7 205 206 mpbir2an ⊢ 𝑆 Or 𝐹