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

Theorem soseq 33545
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 5492 . . . 4 (𝑅 Or (𝐴 ∪ {∅}) → 𝑅 Po (𝐴 ∪ {∅}))
31, 2ax-mp 5 . . 3 𝑅 Po (𝐴 ∪ {∅})
4 soseq.2 . . 3 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴}
5 soseq.3 . . 3 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
63, 4, 5poseq 33544 . 2 𝑆 Po 𝐹
7 eleq1w 2820 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
87anbi1d 633 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
9 fveq1 6721 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
109eqeq1d 2739 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
1110ralbidv 3118 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
12 fveq1 6721 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
1312breq1d 5068 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
1411, 13anbi12d 634 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
1514rexbidv 3221 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
168, 15anbi12d 634 . . . . . . . . . 10 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
17 eleq1w 2820 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
1817anbi2d 632 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
19 fveq1 6721 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
2019eqeq2d 2748 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
2120ralbidv 3118 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦)))
22 fveq1 6721 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → (𝑔𝑥) = (𝑏𝑥))
2322breq2d 5070 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑏𝑥)))
2421, 23anbi12d 634 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2524rexbidv 3221 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2618, 25anbi12d 634 . . . . . . . . . 10 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2716, 26, 5brabg 5425 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2827bianabs 545 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
29 eleq1w 2820 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
3029anbi1d 633 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
31 fveq1 6721 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
3231eqeq1d 2739 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
3332ralbidv 3118 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦)))
34 fveq1 6721 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓𝑥) = (𝑏𝑥))
3534breq1d 5068 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑔𝑥)))
3633, 35anbi12d 634 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3736rexbidv 3221 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3830, 37anbi12d 634 . . . . . . . . . . 11 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)))))
39 eleq1w 2820 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
4039anbi2d 632 . . . . . . . . . . . 12 (𝑔 = 𝑎 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑎𝐹)))
41 fveq1 6721 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
4241eqeq2d 2748 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑎𝑦)))
4342ralbidv 3118 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦)))
44 fveq1 6721 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
4544breq2d 5070 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → ((𝑏𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑎𝑥)))
4643, 45anbi12d 634 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4746rexbidv 3221 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4840, 47anbi12d 634 . . . . . . . . . . 11 (𝑔 = 𝑎 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
4938, 48, 5brabg 5425 . . . . . . . . . 10 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5049bianabs 545 . . . . . . . . 9 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5150ancoms 462 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5228, 51orbi12d 919 . . . . . . 7 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5352notbid 321 . . . . . 6 ((𝑎𝐹𝑏𝐹) → (¬ (𝑎𝑆𝑏𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
54 ralinexa 3188 . . . . . . . 8 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
55 andi 1008 . . . . . . . . . . 11 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
56 eqcom 2744 . . . . . . . . . . . . . 14 ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑏𝑦) = (𝑎𝑦))
5756ralbii 3088 . . . . . . . . . . . . 13 (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦))
5857anbi1i 627 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))
5958orbi2i 913 . . . . . . . . . . 11 (((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6055, 59bitri 278 . . . . . . . . . 10 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6160rexbii 3175 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
62 r19.43 3269 . . . . . . . . 9 (∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6361, 62bitri 278 . . . . . . . 8 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6454, 63xchbinx 337 . . . . . . 7 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
65 feq2 6532 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑓:𝑥𝐴𝑓:𝑦𝐴))
6665cbvrexvw 3364 . . . . . . . . . . . . . 14 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦𝐴)
6766abbii 2808 . . . . . . . . . . . . 13 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
684, 67eqtri 2765 . . . . . . . . . . . 12 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
6968orderseqlem 33543 . . . . . . . . . . 11 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
7068orderseqlem 33543 . . . . . . . . . . 11 (𝑏𝐹 → (𝑏𝑥) ∈ (𝐴 ∪ {∅}))
71 sotrieq 5502 . . . . . . . . . . . 12 ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
721, 71mpan 690 . . . . . . . . . . 11 (((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7369, 70, 72syl2an 599 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7473imbi2d 344 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
7574ralbidv 3118 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
76 vex 3417 . . . . . . . . . . . . . 14 𝑦 ∈ V
77 fveq2 6722 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑎𝑥) = (𝑎𝑦))
78 fveq2 6722 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑏𝑥) = (𝑏𝑦))
7977, 78eqeq12d 2753 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦)))
8076, 79sbcie 3742 . . . . . . . . . . . . 13 ([𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦))
8180ralbii 3088 . . . . . . . . . . . 12 (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦))
8281imbi1i 353 . . . . . . . . . . 11 ((∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
8382ralbii 3088 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
84 tfisg 33510 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
8583, 84sylbir 238 . . . . . . . . 9 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
86 vex 3417 . . . . . . . . . . . . . 14 𝑎 ∈ V
87 feq1 6531 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓:𝑥𝐴𝑎:𝑥𝐴))
8887rexbidv 3221 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴))
8986, 88, 4elab2 3596 . . . . . . . . . . . . 13 (𝑎𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴)
90 feq2 6532 . . . . . . . . . . . . . 14 (𝑥 = 𝑝 → (𝑎:𝑥𝐴𝑎:𝑝𝐴))
9190cbvrexvw 3364 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑎:𝑥𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
9289, 91bitri 278 . . . . . . . . . . . 12 (𝑎𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
93 vex 3417 . . . . . . . . . . . . . 14 𝑏 ∈ V
94 feq1 6531 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓:𝑥𝐴𝑏:𝑥𝐴))
9594rexbidv 3221 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴))
9693, 95, 4elab2 3596 . . . . . . . . . . . . 13 (𝑏𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴)
97 feq2 6532 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑏:𝑥𝐴𝑏:𝑞𝐴))
9897cbvrexvw 3364 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑏:𝑥𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
9996, 98bitri 278 . . . . . . . . . . . 12 (𝑏𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
10092, 99anbi12i 630 . . . . . . . . . . 11 ((𝑎𝐹𝑏𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
101 reeanv 3284 . . . . . . . . . . 11 (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
102100, 101bitr4i 281 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴))
103 onss 7573 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ On → 𝑞 ⊆ On)
104 ssralv 3972 . . . . . . . . . . . . . . . . . . 19 (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
105103, 104syl 17 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
106105ad2antlr 727 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
107 soseq.4 . . . . . . . . . . . . . . . . . . 19 ¬ ∅ ∈ 𝐴
108 fveq2 6722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑎𝑥) = (𝑎𝑝))
109 fveq2 6722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑏𝑥) = (𝑏𝑝))
110108, 109eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑝 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑝) = (𝑏𝑝)))
111110rspcv 3537 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝)))
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝))))
113 ffvelrn 6907 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏:𝑞𝐴𝑝𝑞) → (𝑏𝑝) ∈ 𝐴)
114 fdm 6559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎:𝑝𝐴 → dom 𝑎 = 𝑝)
115 eloni 6228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑝 ∈ On → Ord 𝑝)
116 ordirr 6236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑝 → ¬ 𝑝𝑝)
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ On → ¬ 𝑝𝑝)
118 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎𝑝𝑝))
119118notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝𝑝))
120119biimparc 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑝𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121117, 120sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122 ndmfv 6752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑝 ∈ dom 𝑎 → (𝑎𝑝) = ∅)
123 eqtr2 2761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ∅ = (𝑏𝑝))
124 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝 ∈ On ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
131130adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . 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 7573 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ On → 𝑝 ⊆ On)
142 ssralv 3972 . . . . . . . . . . . . . . . . . . 19 (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
143141, 142syl 17 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
144143ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
145 fveq2 6722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑎𝑥) = (𝑎𝑞))
146 fveq2 6722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑏𝑥) = (𝑏𝑞))
147145, 146eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑞 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑞) = (𝑏𝑞)))
148147rspcv 3537 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞)))
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞))))
150 ffvelrn 6907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎:𝑝𝐴𝑞𝑝) → (𝑎𝑞) ∈ 𝐴)
151 fdm 6559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏:𝑞𝐴 → dom 𝑏 = 𝑞)
152 eloni 6228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑞 ∈ On → Ord 𝑞)
153 ordirr 6236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑞 → ¬ 𝑞𝑞)
154152, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑞 ∈ On → ¬ 𝑞𝑞)
155 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏𝑞𝑞))
156155notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞𝑞))
157156biimparc 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158 ndmfv 6752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑞 ∈ dom 𝑏 → (𝑏𝑞) = ∅)
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
160154, 159sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
161 eqtr 2760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → (𝑎𝑞) = ∅)
162 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163162biimpd 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165164expcom 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏𝑞) = ∅ → ((𝑎𝑞) = (𝑏𝑞) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166165com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
167160, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
168167adantll 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
169151, 168sylan2 596 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6250 . . . . . . . . . . . . . . . . 17 ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
182115, 152, 181syl2an 599 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
183182adantr 484 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
184 3orel13 33380 . . . . . . . . . . . . . . 15 ((¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝) → ((𝑝𝑞𝑝 = 𝑞𝑞𝑝) → 𝑝 = 𝑞))
185180, 183, 184syl6ci 71 . . . . . . . . . . . . . 14 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑝 = 𝑞))
186185, 144jcad 516 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
187 ffn 6550 . . . . . . . . . . . . . . 15 (𝑎:𝑝𝐴𝑎 Fn 𝑝)
188 ffn 6550 . . . . . . . . . . . . . . 15 (𝑏:𝑞𝐴𝑏 Fn 𝑞)
189 eqfnfv2 6858 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝑝𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
190187, 188, 189syl2an 599 . . . . . . . . . . . . . 14 ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
191190adantl 485 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
192186, 191sylibrd 262 . . . . . . . . . . . 12 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
193192ex 416 . . . . . . . . . . 11 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏)))
194193rexlimivv 3216 . . . . . . . . . 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 863 . . . 4 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201 3orcomb 1096 . . . . 5 ((𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏))
202 df-3or 1090 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203201, 202bitr2i 279 . . . 4 (((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
204200, 203sylib 221 . . 3 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
205204rgen2 3124 . 2 𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)
206 df-so 5474 . 2 (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)))
2076, 205, 206mpbir2an 711 1 𝑆 Or 𝐹
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3o 1088   = wceq 1543  wcel 2110  {cab 2714  wral 3061  wrex 3062  [wsbc 3699  cun 3869  wss 3871  c0 4242  {csn 4546   class class class wbr 5058  {copab 5120   Po wpo 5471   Or wor 5472  dom cdm 5556  Ord word 6217  Oncon0 6218   Fn wfn 6380  wf 6381  cfv 6385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pr 5327  ax-un 7528
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-ord 6221  df-on 6222  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-fv 6393
This theorem is referenced by:  sltso  33621
  Copyright terms: Public domain W3C validator