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

Theorem soseq 32060
 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 5204 . . . 4 (𝑅 Or (𝐴 ∪ {∅}) → 𝑅 Po (𝐴 ∪ {∅}))
31, 2ax-mp 5 . . 3 𝑅 Po (𝐴 ∪ {∅})
4 soseq.2 . . 3 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴}
5 soseq.3 . . 3 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
63, 4, 5poseq 32059 . 2 𝑆 Po 𝐹
7 eleq1w 2822 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
87anbi1d 743 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
9 fveq1 6351 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
109eqeq1d 2762 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
1110ralbidv 3124 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
12 fveq1 6351 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
1312breq1d 4814 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
1411, 13anbi12d 749 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
1514rexbidv 3190 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
168, 15anbi12d 749 . . . . . . . . . 10 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
17 eleq1w 2822 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
1817anbi2d 742 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
19 fveq1 6351 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
2019eqeq2d 2770 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
2120ralbidv 3124 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦)))
22 fveq1 6351 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → (𝑔𝑥) = (𝑏𝑥))
2322breq2d 4816 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑏𝑥)))
2421, 23anbi12d 749 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2524rexbidv 3190 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2618, 25anbi12d 749 . . . . . . . . . 10 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2716, 26, 5brabg 5144 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2827bianabs 960 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
29 eleq1w 2822 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
3029anbi1d 743 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
31 fveq1 6351 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
3231eqeq1d 2762 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
3332ralbidv 3124 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦)))
34 fveq1 6351 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓𝑥) = (𝑏𝑥))
3534breq1d 4814 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑔𝑥)))
3633, 35anbi12d 749 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3736rexbidv 3190 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3830, 37anbi12d 749 . . . . . . . . . . 11 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)))))
39 eleq1w 2822 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
4039anbi2d 742 . . . . . . . . . . . 12 (𝑔 = 𝑎 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑎𝐹)))
41 fveq1 6351 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
4241eqeq2d 2770 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑎𝑦)))
4342ralbidv 3124 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦)))
44 fveq1 6351 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
4544breq2d 4816 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → ((𝑏𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑎𝑥)))
4643, 45anbi12d 749 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4746rexbidv 3190 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4840, 47anbi12d 749 . . . . . . . . . . 11 (𝑔 = 𝑎 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
4938, 48, 5brabg 5144 . . . . . . . . . 10 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5049bianabs 960 . . . . . . . . 9 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5150ancoms 468 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5228, 51orbi12d 748 . . . . . . 7 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5352notbid 307 . . . . . 6 ((𝑎𝐹𝑏𝐹) → (¬ (𝑎𝑆𝑏𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
54 ralinexa 3135 . . . . . . . 8 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
55 andi 947 . . . . . . . . . . 11 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
56 eqcom 2767 . . . . . . . . . . . . . 14 ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑏𝑦) = (𝑎𝑦))
5756ralbii 3118 . . . . . . . . . . . . 13 (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦))
5857anbi1i 733 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))
5958orbi2i 542 . . . . . . . . . . 11 (((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6055, 59bitri 264 . . . . . . . . . 10 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6160rexbii 3179 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
62 r19.43 3231 . . . . . . . . 9 (∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6361, 62bitri 264 . . . . . . . 8 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6454, 63xchbinx 323 . . . . . . 7 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
65 feq2 6188 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑓:𝑥𝐴𝑓:𝑦𝐴))
6665cbvrexv 3311 . . . . . . . . . . . . . 14 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦𝐴)
6766abbii 2877 . . . . . . . . . . . . 13 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
684, 67eqtri 2782 . . . . . . . . . . . 12 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
6968orderseqlem 32058 . . . . . . . . . . 11 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
7068orderseqlem 32058 . . . . . . . . . . 11 (𝑏𝐹 → (𝑏𝑥) ∈ (𝐴 ∪ {∅}))
71 sotrieq 5214 . . . . . . . . . . . 12 ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
721, 71mpan 708 . . . . . . . . . . 11 (((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7369, 70, 72syl2an 495 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7473imbi2d 329 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
7574ralbidv 3124 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
76 vex 3343 . . . . . . . . . . . . . 14 𝑦 ∈ V
77 fveq2 6352 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑎𝑥) = (𝑎𝑦))
78 fveq2 6352 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑏𝑥) = (𝑏𝑦))
7977, 78eqeq12d 2775 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦)))
8076, 79sbcie 3611 . . . . . . . . . . . . 13 ([𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦))
8180ralbii 3118 . . . . . . . . . . . 12 (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦))
8281imbi1i 338 . . . . . . . . . . 11 ((∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
8382ralbii 3118 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
84 tfisg 32021 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
8583, 84sylbir 225 . . . . . . . . 9 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
86 vex 3343 . . . . . . . . . . . . . 14 𝑎 ∈ V
87 feq1 6187 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓:𝑥𝐴𝑎:𝑥𝐴))
8887rexbidv 3190 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴))
8986, 88, 4elab2 3494 . . . . . . . . . . . . 13 (𝑎𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴)
90 feq2 6188 . . . . . . . . . . . . . 14 (𝑥 = 𝑝 → (𝑎:𝑥𝐴𝑎:𝑝𝐴))
9190cbvrexv 3311 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑎:𝑥𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
9289, 91bitri 264 . . . . . . . . . . . 12 (𝑎𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
93 vex 3343 . . . . . . . . . . . . . 14 𝑏 ∈ V
94 feq1 6187 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓:𝑥𝐴𝑏:𝑥𝐴))
9594rexbidv 3190 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴))
9693, 95, 4elab2 3494 . . . . . . . . . . . . 13 (𝑏𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴)
97 feq2 6188 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑏:𝑥𝐴𝑏:𝑞𝐴))
9897cbvrexv 3311 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑏:𝑥𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
9996, 98bitri 264 . . . . . . . . . . . 12 (𝑏𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
10092, 99anbi12i 735 . . . . . . . . . . 11 ((𝑎𝐹𝑏𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
101 reeanv 3245 . . . . . . . . . . 11 (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
102100, 101bitr4i 267 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴))
103 onss 7155 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ On → 𝑞 ⊆ On)
104 ssralv 3807 . . . . . . . . . . . . . . . . . . 19 (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
105103, 104syl 17 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
106105ad2antlr 765 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
107 soseq.4 . . . . . . . . . . . . . . . . . . 19 ¬ ∅ ∈ 𝐴
108 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑎𝑥) = (𝑎𝑝))
109 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑏𝑥) = (𝑏𝑝))
110108, 109eqeq12d 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑝 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑝) = (𝑏𝑝)))
111110rspcv 3445 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝)))
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝))))
113 ffvelrn 6520 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏:𝑞𝐴𝑝𝑞) → (𝑏𝑝) ∈ 𝐴)
114 fdm 6212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎:𝑝𝐴 → dom 𝑎 = 𝑝)
115 eloni 5894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑝 ∈ On → Ord 𝑝)
116 ordirr 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑝 → ¬ 𝑝𝑝)
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ On → ¬ 𝑝𝑝)
118 eleq2 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎𝑝𝑝))
119118notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝𝑝))
120119biimparc 505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑝𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121117, 120sylan 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122 ndmfv 6379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑝 ∈ dom 𝑎 → (𝑎𝑝) = ∅)
123 eqtr2 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ∅ = (𝑏𝑝))
124 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∅ = (𝑏𝑝) → (∅ ∈ 𝐴 ↔ (𝑏𝑝) ∈ 𝐴))
125124biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∅ = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
126123, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
127126ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎𝑝) = ∅ → ((𝑎𝑝) = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
128121, 122, 1273syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎𝑝) = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
129128com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
130114, 129sylan2 492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝 ∈ On ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
131130adantlr 753 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
132113, 131syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝𝐴) → ((𝑏:𝑞𝐴𝑝𝑞) → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
133132exp4b 633 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝𝐴 → (𝑏:𝑞𝐴 → (𝑝𝑞 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))))
134133imp32 448 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
135112, 134syldd 72 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → ∅ ∈ 𝐴)))
136135com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑝𝑞 → ∅ ∈ 𝐴)))
137136imp 444 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)) → (𝑝𝑞 → ∅ ∈ 𝐴))
138107, 137mtoi 190 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)) → ¬ 𝑝𝑞)
139138ex 449 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑝𝑞))
140106, 139syld 47 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑝𝑞))
141 onss 7155 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ On → 𝑝 ⊆ On)
142 ssralv 3807 . . . . . . . . . . . . . . . . . . 19 (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
143141, 142syl 17 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
144143ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
145 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑎𝑥) = (𝑎𝑞))
146 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑏𝑥) = (𝑏𝑞))
147145, 146eqeq12d 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑞 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑞) = (𝑏𝑞)))
148147rspcv 3445 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞)))
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞))))
150 ffvelrn 6520 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎:𝑝𝐴𝑞𝑝) → (𝑎𝑞) ∈ 𝐴)
151 fdm 6212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏:𝑞𝐴 → dom 𝑏 = 𝑞)
152 eloni 5894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑞 ∈ On → Ord 𝑞)
153 ordirr 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑞 → ¬ 𝑞𝑞)
154152, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑞 ∈ On → ¬ 𝑞𝑞)
155 eleq2 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏𝑞𝑞))
156155notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞𝑞))
157156biimparc 505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158 ndmfv 6379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑞 ∈ dom 𝑏 → (𝑏𝑞) = ∅)
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
160154, 159sylan 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
161 eqtr 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → (𝑎𝑞) = ∅)
162 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163162biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165164expcom 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏𝑞) = ∅ → ((𝑎𝑞) = (𝑏𝑞) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166165com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
167160, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
168167adantll 752 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
169151, 168sylan2 492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞𝐴) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
170150, 169syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞𝐴) → ((𝑎:𝑝𝐴𝑞𝑝) → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
171170exp4b 633 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞𝐴 → (𝑎:𝑝𝐴 → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))))
172171com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝𝐴 → (𝑏:𝑞𝐴 → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))))
173172imp32 448 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
174149, 173syldd 72 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → ∅ ∈ 𝐴)))
175174com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑞𝑝 → ∅ ∈ 𝐴)))
176175imp 444 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)) → (𝑞𝑝 → ∅ ∈ 𝐴))
177107, 176mtoi 190 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)) → ¬ 𝑞𝑝)
178177ex 449 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑞𝑝))
179144, 178syld 47 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑞𝑝))
180140, 179jcad 556 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝)))
181 ordtri3or 5916 . . . . . . . . . . . . . . . . 17 ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
182115, 152, 181syl2an 495 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
183182adantr 472 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
184 3orel13 31905 . . . . . . . . . . . . . . 15 ((¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝) → ((𝑝𝑞𝑝 = 𝑞𝑞𝑝) → 𝑝 = 𝑞))
185180, 183, 184syl6ci 71 . . . . . . . . . . . . . 14 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑝 = 𝑞))
186185, 144jcad 556 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
187 ffn 6206 . . . . . . . . . . . . . . 15 (𝑎:𝑝𝐴𝑎 Fn 𝑝)
188 ffn 6206 . . . . . . . . . . . . . . 15 (𝑏:𝑞𝐴𝑏 Fn 𝑞)
189 eqfnfv2 6475 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝑝𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
190187, 188, 189syl2an 495 . . . . . . . . . . . . . 14 ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
191190adantl 473 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
192186, 191sylibrd 249 . . . . . . . . . . . 12 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
193192ex 449 . . . . . . . . . . 11 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏)))
194193rexlimivv 3174 . . . . . . . . . 10 (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
195102, 194sylbi 207 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
19685, 195syl5 34 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) → 𝑎 = 𝑏))
19775, 196sylbird 250 . . . . . . 7 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) → 𝑎 = 𝑏))
19864, 197syl5bir 233 . . . . . 6 ((𝑎𝐹𝑏𝐹) → (¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) → 𝑎 = 𝑏))
19953, 198sylbid 230 . . . . 5 ((𝑎𝐹𝑏𝐹) → (¬ (𝑎𝑆𝑏𝑏𝑆𝑎) → 𝑎 = 𝑏))
200199orrd 392 . . . 4 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201 3orcomb 1079 . . . . 5 ((𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏))
202 df-3or 1073 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203201, 202bitr2i 265 . . . 4 (((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
204200, 203sylib 208 . . 3 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
205204rgen2a 3115 . 2 𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)
206 df-so 5188 . 2 (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)))
2076, 205, 206mpbir2an 993 1 𝑆 Or 𝐹
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∨ w3o 1071   = wceq 1632   ∈ wcel 2139  {cab 2746  ∀wral 3050  ∃wrex 3051  [wsbc 3576   ∪ cun 3713   ⊆ wss 3715  ∅c0 4058  {csn 4321   class class class wbr 4804  {copab 4864   Po wpo 5185   Or wor 5186  dom cdm 5266  Ord word 5883  Oncon0 5884   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-ord 5887  df-on 5888  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057 This theorem is referenced by:  sltso  32133
 Copyright terms: Public domain W3C validator