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

Theorem soseq 30995
 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 4976 . . . 4 (𝑅 Or (𝐴 ∪ {∅}) → 𝑅 Po (𝐴 ∪ {∅}))
31, 2ax-mp 5 . . 3 𝑅 Po (𝐴 ∪ {∅})
4 soseq.2 . . 3 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴}
5 soseq.3 . . 3 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
63, 4, 5poseq 30994 . 2 𝑆 Po 𝐹
7 eleq1 2676 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
87anbi1d 737 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
9 fveq1 6102 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
109eqeq1d 2612 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
1110ralbidv 2969 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
12 fveq1 6102 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
1312breq1d 4593 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
1411, 13anbi12d 743 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
1514rexbidv 3034 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
168, 15anbi12d 743 . . . . . . . . . 10 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
17 eleq1 2676 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
1817anbi2d 736 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
19 fveq1 6102 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
2019eqeq2d 2620 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
2120ralbidv 2969 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦)))
22 fveq1 6102 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → (𝑔𝑥) = (𝑏𝑥))
2322breq2d 4595 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑏𝑥)))
2421, 23anbi12d 743 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2524rexbidv 3034 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2618, 25anbi12d 743 . . . . . . . . . 10 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2716, 26, 5brabg 4919 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2827bianabs 920 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
29 eleq1 2676 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
3029anbi1d 737 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
31 fveq1 6102 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
3231eqeq1d 2612 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
3332ralbidv 2969 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦)))
34 fveq1 6102 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓𝑥) = (𝑏𝑥))
3534breq1d 4593 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑔𝑥)))
3633, 35anbi12d 743 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3736rexbidv 3034 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3830, 37anbi12d 743 . . . . . . . . . . 11 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)))))
39 eleq1 2676 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
4039anbi2d 736 . . . . . . . . . . . 12 (𝑔 = 𝑎 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑎𝐹)))
41 fveq1 6102 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
4241eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑎𝑦)))
4342ralbidv 2969 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦)))
44 fveq1 6102 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
4544breq2d 4595 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → ((𝑏𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑎𝑥)))
4643, 45anbi12d 743 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4746rexbidv 3034 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4840, 47anbi12d 743 . . . . . . . . . . 11 (𝑔 = 𝑎 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
4938, 48, 5brabg 4919 . . . . . . . . . 10 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5049bianabs 920 . . . . . . . . 9 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5150ancoms 468 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5228, 51orbi12d 742 . . . . . . 7 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5352notbid 307 . . . . . 6 ((𝑎𝐹𝑏𝐹) → (¬ (𝑎𝑆𝑏𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
54 ralinexa 2980 . . . . . . . 8 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
55 andi 907 . . . . . . . . . . 11 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
56 eqcom 2617 . . . . . . . . . . . . . 14 ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑏𝑦) = (𝑎𝑦))
5756ralbii 2963 . . . . . . . . . . . . 13 (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦))
5857anbi1i 727 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))
5958orbi2i 540 . . . . . . . . . . 11 (((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6055, 59bitri 263 . . . . . . . . . 10 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6160rexbii 3023 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
62 r19.43 3074 . . . . . . . . 9 (∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6361, 62bitri 263 . . . . . . . 8 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6454, 63xchbinx 323 . . . . . . 7 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
65 feq2 5940 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑓:𝑥𝐴𝑓:𝑦𝐴))
6665cbvrexv 3148 . . . . . . . . . . . . . 14 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦𝐴)
6766abbii 2726 . . . . . . . . . . . . 13 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
684, 67eqtri 2632 . . . . . . . . . . . 12 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
6968orderseqlem 30993 . . . . . . . . . . 11 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
7068orderseqlem 30993 . . . . . . . . . . 11 (𝑏𝐹 → (𝑏𝑥) ∈ (𝐴 ∪ {∅}))
71 sotrieq 4986 . . . . . . . . . . . 12 ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
721, 71mpan 702 . . . . . . . . . . 11 (((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7369, 70, 72syl2an 493 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7473imbi2d 329 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
7574ralbidv 2969 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
76 vex 3176 . . . . . . . . . . . . . 14 𝑦 ∈ V
77 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑎𝑥) = (𝑎𝑦))
78 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑏𝑥) = (𝑏𝑦))
7977, 78eqeq12d 2625 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦)))
8076, 79sbcie 3437 . . . . . . . . . . . . 13 ([𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦))
8180ralbii 2963 . . . . . . . . . . . 12 (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦))
8281imbi1i 338 . . . . . . . . . . 11 ((∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
8382ralbii 2963 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
84 tfisg 30960 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
8583, 84sylbir 224 . . . . . . . . 9 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
86 vex 3176 . . . . . . . . . . . . . 14 𝑎 ∈ V
87 feq1 5939 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓:𝑥𝐴𝑎:𝑥𝐴))
8887rexbidv 3034 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴))
8986, 88, 4elab2 3323 . . . . . . . . . . . . 13 (𝑎𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴)
90 feq2 5940 . . . . . . . . . . . . . 14 (𝑥 = 𝑝 → (𝑎:𝑥𝐴𝑎:𝑝𝐴))
9190cbvrexv 3148 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑎:𝑥𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
9289, 91bitri 263 . . . . . . . . . . . 12 (𝑎𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
93 vex 3176 . . . . . . . . . . . . . 14 𝑏 ∈ V
94 feq1 5939 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓:𝑥𝐴𝑏:𝑥𝐴))
9594rexbidv 3034 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴))
9693, 95, 4elab2 3323 . . . . . . . . . . . . 13 (𝑏𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴)
97 feq2 5940 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑏:𝑥𝐴𝑏:𝑞𝐴))
9897cbvrexv 3148 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑏:𝑥𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
9996, 98bitri 263 . . . . . . . . . . . 12 (𝑏𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
10092, 99anbi12i 729 . . . . . . . . . . 11 ((𝑎𝐹𝑏𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
101 reeanv 3086 . . . . . . . . . . 11 (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
102100, 101bitr4i 266 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴))
103 onss 6882 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ On → 𝑞 ⊆ On)
104 ssralv 3629 . . . . . . . . . . . . . . . . . . 19 (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
105103, 104syl 17 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
106105ad2antlr 759 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
107 soseq.4 . . . . . . . . . . . . . . . . . . 19 ¬ ∅ ∈ 𝐴
108 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑎𝑥) = (𝑎𝑝))
109 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑏𝑥) = (𝑏𝑝))
110108, 109eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑝 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑝) = (𝑏𝑝)))
111110rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝)))
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝))))
113 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏:𝑞𝐴𝑝𝑞) → (𝑏𝑝) ∈ 𝐴)
114 fdm 5964 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎:𝑝𝐴 → dom 𝑎 = 𝑝)
115 eloni 5650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑝 ∈ On → Ord 𝑝)
116 ordirr 5658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑝 → ¬ 𝑝𝑝)
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ On → ¬ 𝑝𝑝)
118 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎𝑝𝑝))
119118notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝𝑝))
120119biimparc 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑝𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121117, 120sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122 ndmfv 6128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑝 ∈ dom 𝑎 → (𝑎𝑝) = ∅)
123 eqtr2 2630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ∅ = (𝑏𝑝))
124 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∅ = (𝑏𝑝) → (∅ ∈ 𝐴 ↔ (𝑏𝑝) ∈ 𝐴))
125124biimprd 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∅ = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
126123, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
127126ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎𝑝) = ∅ → ((𝑎𝑝) = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
128121, 122, 1273syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎𝑝) = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
129128com23 84 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
130114, 129sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝 ∈ On ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
131130adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
132113, 131syl5 33 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝𝐴) → ((𝑏:𝑞𝐴𝑝𝑞) → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
133132exp4b 630 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝𝐴 → (𝑏:𝑞𝐴 → (𝑝𝑞 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))))
134133imp32 448 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
135112, 134syldd 70 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → ∅ ∈ 𝐴)))
136135com23 84 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑝𝑞 → ∅ ∈ 𝐴)))
137136imp 444 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)) → (𝑝𝑞 → ∅ ∈ 𝐴))
138107, 137mtoi 189 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)) → ¬ 𝑝𝑞)
139138ex 449 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑝𝑞))
140106, 139syld 46 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑝𝑞))
141 onss 6882 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ On → 𝑝 ⊆ On)
142 ssralv 3629 . . . . . . . . . . . . . . . . . . 19 (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
143141, 142syl 17 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
144143ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
145 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑎𝑥) = (𝑎𝑞))
146 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑏𝑥) = (𝑏𝑞))
147145, 146eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑞 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑞) = (𝑏𝑞)))
148147rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞)))
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞))))
150 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎:𝑝𝐴𝑞𝑝) → (𝑎𝑞) ∈ 𝐴)
151 fdm 5964 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏:𝑞𝐴 → dom 𝑏 = 𝑞)
152 eloni 5650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑞 ∈ On → Ord 𝑞)
153 ordirr 5658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑞 → ¬ 𝑞𝑞)
154152, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑞 ∈ On → ¬ 𝑞𝑞)
155 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏𝑞𝑞))
156155notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞𝑞))
157156biimparc 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158 ndmfv 6128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑞 ∈ dom 𝑏 → (𝑏𝑞) = ∅)
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
160154, 159sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
161 eqtr 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → (𝑎𝑞) = ∅)
162 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163162biimpd 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165164expcom 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏𝑞) = ∅ → ((𝑎𝑞) = (𝑏𝑞) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166165com23 84 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
167160, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
168167adantll 746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
169151, 168sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞𝐴) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
170150, 169syl5 33 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞𝐴) → ((𝑎:𝑝𝐴𝑞𝑝) → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
171170exp4b 630 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞𝐴 → (𝑎:𝑝𝐴 → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))))
172171com23 84 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝𝐴 → (𝑏:𝑞𝐴 → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))))
173172imp32 448 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
174149, 173syldd 70 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → ∅ ∈ 𝐴)))
175174com23 84 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑞𝑝 → ∅ ∈ 𝐴)))
176175imp 444 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)) → (𝑞𝑝 → ∅ ∈ 𝐴))
177107, 176mtoi 189 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)) → ¬ 𝑞𝑝)
178177ex 449 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑞𝑝))
179144, 178syld 46 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑞𝑝))
180140, 179jcad 554 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝)))
181 ordtri3or 5672 . . . . . . . . . . . . . . . . 17 ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
182115, 152, 181syl2an 493 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
183182adantr 480 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
184 3orel13 30853 . . . . . . . . . . . . . . 15 ((¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝) → ((𝑝𝑞𝑝 = 𝑞𝑞𝑝) → 𝑝 = 𝑞))
185180, 183, 184syl6ci 69 . . . . . . . . . . . . . 14 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑝 = 𝑞))
186185, 144jcad 554 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
187 ffn 5958 . . . . . . . . . . . . . . 15 (𝑎:𝑝𝐴𝑎 Fn 𝑝)
188 ffn 5958 . . . . . . . . . . . . . . 15 (𝑏:𝑞𝐴𝑏 Fn 𝑞)
189 eqfnfv2 6220 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝑝𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
190187, 188, 189syl2an 493 . . . . . . . . . . . . . 14 ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
191190adantl 481 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
192186, 191sylibrd 248 . . . . . . . . . . . 12 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
193192ex 449 . . . . . . . . . . 11 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏)))
194193rexlimivv 3018 . . . . . . . . . 10 (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
195102, 194sylbi 206 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
19685, 195syl5 33 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) → 𝑎 = 𝑏))
19775, 196sylbird 249 . . . . . . 7 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) → 𝑎 = 𝑏))
19864, 197syl5bir 232 . . . . . 6 ((𝑎𝐹𝑏𝐹) → (¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) → 𝑎 = 𝑏))
19953, 198sylbid 229 . . . . 5 ((𝑎𝐹𝑏𝐹) → (¬ (𝑎𝑆𝑏𝑏𝑆𝑎) → 𝑎 = 𝑏))
200199orrd 392 . . . 4 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201 3orcomb 1041 . . . . 5 ((𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏))
202 df-3or 1032 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203201, 202bitr2i 264 . . . 4 (((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
204200, 203sylib 207 . . 3 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
205204rgen2a 2960 . 2 𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)
206 df-so 4960 . 2 (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)))
2076, 205, 206mpbir2an 957 1 𝑆 Or 𝐹
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897  [wsbc 3402   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583  {copab 4642   Po wpo 4957   Or wor 4958  dom cdm 5038  Ord word 5639  Oncon0 5640   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812 This theorem is referenced by:  sltso  31068
 Copyright terms: Public domain W3C validator