Metamath Proof Explorer


Theorem soseq

Description: A linear ordering of sequences of ordinals. (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 ffvelrn ( ( 𝑏 : 𝑞𝐴𝑝𝑞 ) → ( 𝑏𝑝 ) ∈ 𝐴 )
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 ffvelrn ( ( 𝑎 : 𝑝𝐴𝑞𝑝 ) → ( 𝑎𝑞 ) ∈ 𝐴 )
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 syl5bir ( ( 𝑎𝐹𝑏𝐹 ) → ( ¬ ( ∃ 𝑥 ∈ 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 𝐹