Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  soseq Structured version   Visualization version   GIF version

Theorem soseq 33104
 Description: A linear ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.)
Hypotheses
Ref Expression
soseq.1 𝑅 Or (𝐴 ∪ {∅})
soseq.2 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴}
soseq.3 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
soseq.4 ¬ ∅ ∈ 𝐴
Assertion
Ref Expression
soseq 𝑆 Or 𝐹
Distinct variable groups:   𝐴,𝑓,𝑥,𝑦   𝑓,𝐹,𝑔,𝑥   𝑦,𝑓,𝑔,𝑥   𝑅,𝑓,𝑔,𝑥
Allowed substitution hints:   𝐴(𝑔)   𝑅(𝑦)   𝑆(𝑥,𝑦,𝑓,𝑔)   𝐹(𝑦)

Proof of Theorem soseq
Dummy variables 𝑎 𝑏 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 soseq.1 . . . 4 𝑅 Or (𝐴 ∪ {∅})
2 sopo 5465 . . . 4 (𝑅 Or (𝐴 ∪ {∅}) → 𝑅 Po (𝐴 ∪ {∅}))
31, 2ax-mp 5 . . 3 𝑅 Po (𝐴 ∪ {∅})
4 soseq.2 . . 3 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴}
5 soseq.3 . . 3 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
63, 4, 5poseq 33103 . 2 𝑆 Po 𝐹
7 eleq1w 2894 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
87anbi1d 632 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
9 fveq1 6642 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
109eqeq1d 2823 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
1110ralbidv 3185 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
12 fveq1 6642 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
1312breq1d 5049 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
1411, 13anbi12d 633 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
1514rexbidv 3283 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
168, 15anbi12d 633 . . . . . . . . . 10 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
17 eleq1w 2894 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
1817anbi2d 631 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
19 fveq1 6642 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
2019eqeq2d 2832 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
2120ralbidv 3185 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦)))
22 fveq1 6642 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → (𝑔𝑥) = (𝑏𝑥))
2322breq2d 5051 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑏𝑥)))
2421, 23anbi12d 633 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2524rexbidv 3283 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2618, 25anbi12d 633 . . . . . . . . . 10 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2716, 26, 5brabg 5399 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2827bianabs 545 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
29 eleq1w 2894 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
3029anbi1d 632 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
31 fveq1 6642 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
3231eqeq1d 2823 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
3332ralbidv 3185 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦)))
34 fveq1 6642 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓𝑥) = (𝑏𝑥))
3534breq1d 5049 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑔𝑥)))
3633, 35anbi12d 633 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3736rexbidv 3283 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3830, 37anbi12d 633 . . . . . . . . . . 11 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)))))
39 eleq1w 2894 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
4039anbi2d 631 . . . . . . . . . . . 12 (𝑔 = 𝑎 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑎𝐹)))
41 fveq1 6642 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
4241eqeq2d 2832 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑎𝑦)))
4342ralbidv 3185 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦)))
44 fveq1 6642 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
4544breq2d 5051 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → ((𝑏𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑎𝑥)))
4643, 45anbi12d 633 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4746rexbidv 3283 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4840, 47anbi12d 633 . . . . . . . . . . 11 (𝑔 = 𝑎 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
4938, 48, 5brabg 5399 . . . . . . . . . 10 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5049bianabs 545 . . . . . . . . 9 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5150ancoms 462 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5228, 51orbi12d 916 . . . . . . 7 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5352notbid 321 . . . . . 6 ((𝑎𝐹𝑏𝐹) → (¬ (𝑎𝑆𝑏𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
54 ralinexa 3250 . . . . . . . 8 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
55 andi 1005 . . . . . . . . . . 11 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
56 eqcom 2828 . . . . . . . . . . . . . 14 ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑏𝑦) = (𝑎𝑦))
5756ralbii 3153 . . . . . . . . . . . . 13 (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦))
5857anbi1i 626 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))
5958orbi2i 910 . . . . . . . . . . 11 (((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6055, 59bitri 278 . . . . . . . . . 10 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6160rexbii 3235 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
62 r19.43 3336 . . . . . . . . 9 (∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6361, 62bitri 278 . . . . . . . 8 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6454, 63xchbinx 337 . . . . . . 7 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
65 feq2 6469 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑓:𝑥𝐴𝑓:𝑦𝐴))
6665cbvrexvw 3427 . . . . . . . . . . . . . 14 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦𝐴)
6766abbii 2886 . . . . . . . . . . . . 13 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
684, 67eqtri 2844 . . . . . . . . . . . 12 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
6968orderseqlem 33102 . . . . . . . . . . 11 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
7068orderseqlem 33102 . . . . . . . . . . 11 (𝑏𝐹 → (𝑏𝑥) ∈ (𝐴 ∪ {∅}))
71 sotrieq 5475 . . . . . . . . . . . 12 ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
721, 71mpan 689 . . . . . . . . . . 11 (((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7369, 70, 72syl2an 598 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7473imbi2d 344 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
7574ralbidv 3185 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
76 vex 3474 . . . . . . . . . . . . . 14 𝑦 ∈ V
77 fveq2 6643 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑎𝑥) = (𝑎𝑦))
78 fveq2 6643 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑏𝑥) = (𝑏𝑦))
7977, 78eqeq12d 2837 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦)))
8076, 79sbcie 3789 . . . . . . . . . . . . 13 ([𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦))
8180ralbii 3153 . . . . . . . . . . . 12 (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦))
8281imbi1i 353 . . . . . . . . . . 11 ((∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
8382ralbii 3153 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
84 tfisg 33063 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
8583, 84sylbir 238 . . . . . . . . 9 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
86 vex 3474 . . . . . . . . . . . . . 14 𝑎 ∈ V
87 feq1 6468 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓:𝑥𝐴𝑎:𝑥𝐴))
8887rexbidv 3283 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴))
8986, 88, 4elab2 3647 . . . . . . . . . . . . 13 (𝑎𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴)
90 feq2 6469 . . . . . . . . . . . . . 14 (𝑥 = 𝑝 → (𝑎:𝑥𝐴𝑎:𝑝𝐴))
9190cbvrexvw 3427 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑎:𝑥𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
9289, 91bitri 278 . . . . . . . . . . . 12 (𝑎𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
93 vex 3474 . . . . . . . . . . . . . 14 𝑏 ∈ V
94 feq1 6468 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓:𝑥𝐴𝑏:𝑥𝐴))
9594rexbidv 3283 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴))
9693, 95, 4elab2 3647 . . . . . . . . . . . . 13 (𝑏𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴)
97 feq2 6469 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑏:𝑥𝐴𝑏:𝑞𝐴))
9897cbvrexvw 3427 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑏:𝑥𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
9996, 98bitri 278 . . . . . . . . . . . 12 (𝑏𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
10092, 99anbi12i 629 . . . . . . . . . . 11 ((𝑎𝐹𝑏𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
101 reeanv 3352 . . . . . . . . . . 11 (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
102100, 101bitr4i 281 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴))
103 onss 7480 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ On → 𝑞 ⊆ On)
104 ssralv 4009 . . . . . . . . . . . . . . . . . . 19 (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
105103, 104syl 17 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
106105ad2antlr 726 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
107 soseq.4 . . . . . . . . . . . . . . . . . . 19 ¬ ∅ ∈ 𝐴
108 fveq2 6643 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑎𝑥) = (𝑎𝑝))
109 fveq2 6643 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑏𝑥) = (𝑏𝑝))
110108, 109eqeq12d 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑝 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑝) = (𝑏𝑝)))
111110rspcv 3595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝)))
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝))))
113 ffvelrn 6822 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏:𝑞𝐴𝑝𝑞) → (𝑏𝑝) ∈ 𝐴)
114 fdm 6495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎:𝑝𝐴 → dom 𝑎 = 𝑝)
115 eloni 6174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑝 ∈ On → Ord 𝑝)
116 ordirr 6182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑝 → ¬ 𝑝𝑝)
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ On → ¬ 𝑝𝑝)
118 eleq2 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎𝑝𝑝))
119118notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝𝑝))
120119biimparc 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑝𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121117, 120sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122 ndmfv 6673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑝 ∈ dom 𝑎 → (𝑎𝑝) = ∅)
123 eqtr2 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ∅ = (𝑏𝑝))
124 eleq1 2899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∅ = (𝑏𝑝) → (∅ ∈ 𝐴 ↔ (𝑏𝑝) ∈ 𝐴))
125124biimprd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∅ = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
126123, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
127126ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎𝑝) = ∅ → ((𝑎𝑝) = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
128121, 122, 1273syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎𝑝) = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
129128com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
130114, 129sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝 ∈ On ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
131130adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
132113, 131syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝𝐴) → ((𝑏:𝑞𝐴𝑝𝑞) → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
133132exp4b 434 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝𝐴 → (𝑏:𝑞𝐴 → (𝑝𝑞 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))))
134133imp32 422 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
135112, 134syldd 72 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → ∅ ∈ 𝐴)))
136135com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑝𝑞 → ∅ ∈ 𝐴)))
137136imp 410 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)) → (𝑝𝑞 → ∅ ∈ 𝐴))
138107, 137mtoi 202 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)) → ¬ 𝑝𝑞)
139138ex 416 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑝𝑞))
140106, 139syld 47 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑝𝑞))
141 onss 7480 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ On → 𝑝 ⊆ On)
142 ssralv 4009 . . . . . . . . . . . . . . . . . . 19 (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
143141, 142syl 17 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
144143ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
145 fveq2 6643 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑎𝑥) = (𝑎𝑞))
146 fveq2 6643 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑏𝑥) = (𝑏𝑞))
147145, 146eqeq12d 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑞 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑞) = (𝑏𝑞)))
148147rspcv 3595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞)))
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞))))
150 ffvelrn 6822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎:𝑝𝐴𝑞𝑝) → (𝑎𝑞) ∈ 𝐴)
151 fdm 6495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏:𝑞𝐴 → dom 𝑏 = 𝑞)
152 eloni 6174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑞 ∈ On → Ord 𝑞)
153 ordirr 6182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑞 → ¬ 𝑞𝑞)
154152, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑞 ∈ On → ¬ 𝑞𝑞)
155 eleq2 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏𝑞𝑞))
156155notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞𝑞))
157156biimparc 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158 ndmfv 6673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑞 ∈ dom 𝑏 → (𝑏𝑞) = ∅)
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
160154, 159sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
161 eqtr 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → (𝑎𝑞) = ∅)
162 eleq1 2899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163162biimpd 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165164expcom 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏𝑞) = ∅ → ((𝑎𝑞) = (𝑏𝑞) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166165com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
167160, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
168167adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
169151, 168sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞𝐴) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
170150, 169syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞𝐴) → ((𝑎:𝑝𝐴𝑞𝑝) → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
171170exp4b 434 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞𝐴 → (𝑎:𝑝𝐴 → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))))
172171com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝𝐴 → (𝑏:𝑞𝐴 → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))))
173172imp32 422 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
174149, 173syldd 72 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → ∅ ∈ 𝐴)))
175174com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑞𝑝 → ∅ ∈ 𝐴)))
176175imp 410 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)) → (𝑞𝑝 → ∅ ∈ 𝐴))
177107, 176mtoi 202 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)) → ¬ 𝑞𝑝)
178177ex 416 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑞𝑝))
179144, 178syld 47 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑞𝑝))
180140, 179jcad 516 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝)))
181 ordtri3or 6196 . . . . . . . . . . . . . . . . 17 ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
182115, 152, 181syl2an 598 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
183182adantr 484 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
184 3orel13 32955 . . . . . . . . . . . . . . 15 ((¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝) → ((𝑝𝑞𝑝 = 𝑞𝑞𝑝) → 𝑝 = 𝑞))
185180, 183, 184syl6ci 71 . . . . . . . . . . . . . 14 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑝 = 𝑞))
186185, 144jcad 516 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
187 ffn 6487 . . . . . . . . . . . . . . 15 (𝑎:𝑝𝐴𝑎 Fn 𝑝)
188 ffn 6487 . . . . . . . . . . . . . . 15 (𝑏:𝑞𝐴𝑏 Fn 𝑞)
189 eqfnfv2 6776 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝑝𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
190187, 188, 189syl2an 598 . . . . . . . . . . . . . 14 ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
191190adantl 485 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
192186, 191sylibrd 262 . . . . . . . . . . . 12 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
193192ex 416 . . . . . . . . . . 11 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏)))
194193rexlimivv 3278 . . . . . . . . . 10 (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
195102, 194sylbi 220 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
19685, 195syl5 34 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) → 𝑎 = 𝑏))
19775, 196sylbird 263 . . . . . . 7 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) → 𝑎 = 𝑏))
19864, 197syl5bir 246 . . . . . 6 ((𝑎𝐹𝑏𝐹) → (¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) → 𝑎 = 𝑏))
19953, 198sylbid 243 . . . . 5 ((𝑎𝐹𝑏𝐹) → (¬ (𝑎𝑆𝑏𝑏𝑆𝑎) → 𝑎 = 𝑏))
200199orrd 860 . . . 4 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201 3orcomb 1091 . . . . 5 ((𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏))
202 df-3or 1085 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203201, 202bitr2i 279 . . . 4 (((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
204200, 203sylib 221 . . 3 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
205204rgen2 3191 . 2 𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)
206 df-so 5448 . 2 (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)))
2076, 205, 206mpbir2an 710 1 𝑆 Or 𝐹
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∨ w3o 1083   = wceq 1538   ∈ wcel 2115  {cab 2799  ∀wral 3126  ∃wrex 3127  [wsbc 3749   ∪ cun 3908   ⊆ wss 3910  ∅c0 4266  {csn 4540   class class class wbr 5039  {copab 5101   Po wpo 5445   Or wor 5446  dom cdm 5528  Ord word 6163  Oncon0 6164   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-ord 6167  df-on 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336 This theorem is referenced by:  sltso  33189
 Copyright terms: Public domain W3C validator