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 31487
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 5017 . . . 4 (𝑅 Or (𝐴 ∪ {∅}) → 𝑅 Po (𝐴 ∪ {∅}))
31, 2ax-mp 5 . . 3 𝑅 Po (𝐴 ∪ {∅})
4 soseq.2 . . 3 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴}
5 soseq.3 . . 3 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)))}
63, 4, 5poseq 31486 . 2 𝑆 Po 𝐹
7 eleq1 2686 . . . . . . . . . . . 12 (𝑓 = 𝑎 → (𝑓𝐹𝑎𝐹))
87anbi1d 740 . . . . . . . . . . 11 (𝑓 = 𝑎 → ((𝑓𝐹𝑔𝐹) ↔ (𝑎𝐹𝑔𝐹)))
9 fveq1 6152 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓𝑦) = (𝑎𝑦))
109eqeq1d 2623 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑔𝑦)))
1110ralbidv 2981 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦)))
12 fveq1 6152 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (𝑓𝑥) = (𝑎𝑥))
1312breq1d 4628 . . . . . . . . . . . . 13 (𝑓 = 𝑎 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑔𝑥)))
1411, 13anbi12d 746 . . . . . . . . . . . 12 (𝑓 = 𝑎 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
1514rexbidv 3046 . . . . . . . . . . 11 (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))))
168, 15anbi12d 746 . . . . . . . . . 10 (𝑓 = 𝑎 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)))))
17 eleq1 2686 . . . . . . . . . . . 12 (𝑔 = 𝑏 → (𝑔𝐹𝑏𝐹))
1817anbi2d 739 . . . . . . . . . . 11 (𝑔 = 𝑏 → ((𝑎𝐹𝑔𝐹) ↔ (𝑎𝐹𝑏𝐹)))
19 fveq1 6152 . . . . . . . . . . . . . . 15 (𝑔 = 𝑏 → (𝑔𝑦) = (𝑏𝑦))
2019eqeq2d 2631 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → ((𝑎𝑦) = (𝑔𝑦) ↔ (𝑎𝑦) = (𝑏𝑦)))
2120ralbidv 2981 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦)))
22 fveq1 6152 . . . . . . . . . . . . . 14 (𝑔 = 𝑏 → (𝑔𝑥) = (𝑏𝑥))
2322breq2d 4630 . . . . . . . . . . . . 13 (𝑔 = 𝑏 → ((𝑎𝑥)𝑅(𝑔𝑥) ↔ (𝑎𝑥)𝑅(𝑏𝑥)))
2421, 23anbi12d 746 . . . . . . . . . . . 12 (𝑔 = 𝑏 → ((∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2524rexbidv 3046 . . . . . . . . . . 11 (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
2618, 25anbi12d 746 . . . . . . . . . 10 (𝑔 = 𝑏 → (((𝑎𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑔𝑦) ∧ (𝑎𝑥)𝑅(𝑔𝑥))) ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2716, 26, 5brabg 4959 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎𝐹𝑏𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)))))
2827bianabs 923 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥))))
29 eleq1 2686 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → (𝑓𝐹𝑏𝐹))
3029anbi1d 740 . . . . . . . . . . . 12 (𝑓 = 𝑏 → ((𝑓𝐹𝑔𝐹) ↔ (𝑏𝐹𝑔𝐹)))
31 fveq1 6152 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
3231eqeq1d 2623 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑔𝑦)))
3332ralbidv 2981 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦)))
34 fveq1 6152 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓𝑥) = (𝑏𝑥))
3534breq1d 4628 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑔𝑥)))
3633, 35anbi12d 746 . . . . . . . . . . . . 13 (𝑓 = 𝑏 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3736rexbidv 3046 . . . . . . . . . . . 12 (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))))
3830, 37anbi12d 746 . . . . . . . . . . 11 (𝑓 = 𝑏 → (((𝑓𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)))))
39 eleq1 2686 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → (𝑔𝐹𝑎𝐹))
4039anbi2d 739 . . . . . . . . . . . 12 (𝑔 = 𝑎 → ((𝑏𝐹𝑔𝐹) ↔ (𝑏𝐹𝑎𝐹)))
41 fveq1 6152 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑎 → (𝑔𝑦) = (𝑎𝑦))
4241eqeq2d 2631 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → ((𝑏𝑦) = (𝑔𝑦) ↔ (𝑏𝑦) = (𝑎𝑦)))
4342ralbidv 2981 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦)))
44 fveq1 6152 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (𝑔𝑥) = (𝑎𝑥))
4544breq2d 4630 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → ((𝑏𝑥)𝑅(𝑔𝑥) ↔ (𝑏𝑥)𝑅(𝑎𝑥)))
4643, 45anbi12d 746 . . . . . . . . . . . . 13 (𝑔 = 𝑎 → ((∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4746rexbidv 3046 . . . . . . . . . . . 12 (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
4840, 47anbi12d 746 . . . . . . . . . . 11 (𝑔 = 𝑎 → (((𝑏𝐹𝑔𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑔𝑦) ∧ (𝑏𝑥)𝑅(𝑔𝑥))) ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
4938, 48, 5brabg 4959 . . . . . . . . . 10 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏𝐹𝑎𝐹) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5049bianabs 923 . . . . . . . . 9 ((𝑏𝐹𝑎𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5150ancoms 469 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
5228, 51orbi12d 745 . . . . . . 7 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
5352notbid 308 . . . . . 6 ((𝑎𝐹𝑏𝐹) → (¬ (𝑎𝑆𝑏𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))))
54 ralinexa 2992 . . . . . . . 8 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
55 andi 910 . . . . . . . . . . 11 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
56 eqcom 2628 . . . . . . . . . . . . . 14 ((𝑎𝑦) = (𝑏𝑦) ↔ (𝑏𝑦) = (𝑎𝑦))
5756ralbii 2975 . . . . . . . . . . . . 13 (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ↔ ∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦))
5857anbi1i 730 . . . . . . . . . . . 12 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)) ↔ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥)))
5958orbi2i 541 . . . . . . . . . . 11 (((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6055, 59bitri 264 . . . . . . . . . 10 ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6160rexbii 3035 . . . . . . . . 9 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
62 r19.43 3086 . . . . . . . . 9 (∃𝑥 ∈ On ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6361, 62bitri 264 . . . . . . . 8 (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
6454, 63xchbinx 324 . . . . . . 7 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) ∧ (𝑎𝑥)𝑅(𝑏𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑏𝑦) = (𝑎𝑦) ∧ (𝑏𝑥)𝑅(𝑎𝑥))))
65 feq2 5989 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑓:𝑥𝐴𝑓:𝑦𝐴))
6665cbvrexv 3163 . . . . . . . . . . . . . 14 (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦𝐴)
6766abbii 2736 . . . . . . . . . . . . 13 {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
684, 67eqtri 2643 . . . . . . . . . . . 12 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦𝐴}
6968orderseqlem 31485 . . . . . . . . . . 11 (𝑎𝐹 → (𝑎𝑥) ∈ (𝐴 ∪ {∅}))
7068orderseqlem 31485 . . . . . . . . . . 11 (𝑏𝐹 → (𝑏𝑥) ∈ (𝐴 ∪ {∅}))
71 sotrieq 5027 . . . . . . . . . . . 12 ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
721, 71mpan 705 . . . . . . . . . . 11 (((𝑎𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7369, 70, 72syl2an 494 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑥) = (𝑏𝑥) ↔ ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥))))
7473imbi2d 330 . . . . . . . . 9 ((𝑎𝐹𝑏𝐹) → ((∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
7574ralbidv 2981 . . . . . . . 8 ((𝑎𝐹𝑏𝐹) → (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → ¬ ((𝑎𝑥)𝑅(𝑏𝑥) ∨ (𝑏𝑥)𝑅(𝑎𝑥)))))
76 vex 3192 . . . . . . . . . . . . . 14 𝑦 ∈ V
77 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑎𝑥) = (𝑎𝑦))
78 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑏𝑥) = (𝑏𝑦))
7977, 78eqeq12d 2636 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦)))
8076, 79sbcie 3456 . . . . . . . . . . . . 13 ([𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑦) = (𝑏𝑦))
8180ralbii 2975 . . . . . . . . . . . 12 (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) ↔ ∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦))
8281imbi1i 339 . . . . . . . . . . 11 ((∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
8382ralbii 2975 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)))
84 tfisg 31452 . . . . . . . . . 10 (∀𝑥 ∈ On (∀𝑦𝑥 [𝑦 / 𝑥](𝑎𝑥) = (𝑏𝑥) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
8583, 84sylbir 225 . . . . . . . . 9 (∀𝑥 ∈ On (∀𝑦𝑥 (𝑎𝑦) = (𝑏𝑦) → (𝑎𝑥) = (𝑏𝑥)) → ∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥))
86 vex 3192 . . . . . . . . . . . . . 14 𝑎 ∈ V
87 feq1 5988 . . . . . . . . . . . . . . 15 (𝑓 = 𝑎 → (𝑓:𝑥𝐴𝑎:𝑥𝐴))
8887rexbidv 3046 . . . . . . . . . . . . . 14 (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴))
8986, 88, 4elab2 3341 . . . . . . . . . . . . 13 (𝑎𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥𝐴)
90 feq2 5989 . . . . . . . . . . . . . 14 (𝑥 = 𝑝 → (𝑎:𝑥𝐴𝑎:𝑝𝐴))
9190cbvrexv 3163 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑎:𝑥𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
9289, 91bitri 264 . . . . . . . . . . . 12 (𝑎𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝𝐴)
93 vex 3192 . . . . . . . . . . . . . 14 𝑏 ∈ V
94 feq1 5988 . . . . . . . . . . . . . . 15 (𝑓 = 𝑏 → (𝑓:𝑥𝐴𝑏:𝑥𝐴))
9594rexbidv 3046 . . . . . . . . . . . . . 14 (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴))
9693, 95, 4elab2 3341 . . . . . . . . . . . . 13 (𝑏𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥𝐴)
97 feq2 5989 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑏:𝑥𝐴𝑏:𝑞𝐴))
9897cbvrexv 3163 . . . . . . . . . . . . 13 (∃𝑥 ∈ On 𝑏:𝑥𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
9996, 98bitri 264 . . . . . . . . . . . 12 (𝑏𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞𝐴)
10092, 99anbi12i 732 . . . . . . . . . . 11 ((𝑎𝐹𝑏𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
101 reeanv 3100 . . . . . . . . . . 11 (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞𝐴))
102100, 101bitr4i 267 . . . . . . . . . 10 ((𝑎𝐹𝑏𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝𝐴𝑏:𝑞𝐴))
103 onss 6944 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ On → 𝑞 ⊆ On)
104 ssralv 3650 . . . . . . . . . . . . . . . . . . 19 (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
105103, 104syl 17 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
106105ad2antlr 762 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)))
107 soseq.4 . . . . . . . . . . . . . . . . . . 19 ¬ ∅ ∈ 𝐴
108 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑎𝑥) = (𝑎𝑝))
109 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑝 → (𝑏𝑥) = (𝑏𝑝))
110108, 109eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑝 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑝) = (𝑏𝑝)))
111110rspcv 3294 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝)))
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑝) = (𝑏𝑝))))
113 ffvelrn 6318 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏:𝑞𝐴𝑝𝑞) → (𝑏𝑝) ∈ 𝐴)
114 fdm 6013 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎:𝑝𝐴 → dom 𝑎 = 𝑝)
115 eloni 5697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑝 ∈ On → Ord 𝑝)
116 ordirr 5705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑝 → ¬ 𝑝𝑝)
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ On → ¬ 𝑝𝑝)
118 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎𝑝𝑝))
119118notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝𝑝))
120119biimparc 504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑝𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121117, 120sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122 ndmfv 6180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑝 ∈ dom 𝑎 → (𝑎𝑝) = ∅)
123 eqtr2 2641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ∅ = (𝑏𝑝))
124 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∅ = (𝑏𝑝) → (∅ ∈ 𝐴 ↔ (𝑏𝑝) ∈ 𝐴))
125124biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∅ = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
126123, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑎𝑝) = ∅ ∧ (𝑎𝑝) = (𝑏𝑝)) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
127126ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎𝑝) = ∅ → ((𝑎𝑝) = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
128121, 122, 1273syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎𝑝) = (𝑏𝑝) → ((𝑏𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
129128com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
130114, 129sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝 ∈ On ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
131130adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝𝐴) → ((𝑏𝑝) ∈ 𝐴 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
132113, 131syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝𝐴) → ((𝑏:𝑞𝐴𝑝𝑞) → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
133132exp4b 631 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝𝐴 → (𝑏:𝑞𝐴 → (𝑝𝑞 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))))
134133imp32 449 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → ((𝑎𝑝) = (𝑏𝑝) → ∅ ∈ 𝐴)))
135112, 134syldd 72 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞 → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → ∅ ∈ 𝐴)))
136135com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → (𝑝𝑞 → ∅ ∈ 𝐴)))
137136imp 445 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)) → (𝑝𝑞 → ∅ ∈ 𝐴))
138107, 137mtoi 190 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥)) → ¬ 𝑝𝑞)
139138ex 450 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑞 (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑝𝑞))
140106, 139syld 47 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑝𝑞))
141 onss 6944 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ On → 𝑝 ⊆ On)
142 ssralv 3650 . . . . . . . . . . . . . . . . . . 19 (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
143141, 142syl 17 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
144143ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)))
145 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑎𝑥) = (𝑎𝑞))
146 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑞 → (𝑏𝑥) = (𝑏𝑞))
147145, 146eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑞 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝑎𝑞) = (𝑏𝑞)))
148147rspcv 3294 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞)))
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑎𝑞) = (𝑏𝑞))))
150 ffvelrn 6318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎:𝑝𝐴𝑞𝑝) → (𝑎𝑞) ∈ 𝐴)
151 fdm 6013 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏:𝑞𝐴 → dom 𝑏 = 𝑞)
152 eloni 5697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑞 ∈ On → Ord 𝑞)
153 ordirr 5705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Ord 𝑞 → ¬ 𝑞𝑞)
154152, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑞 ∈ On → ¬ 𝑞𝑞)
155 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏𝑞𝑞))
156155notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞𝑞))
157156biimparc 504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158 ndmfv 6180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑞 ∈ dom 𝑏 → (𝑏𝑞) = ∅)
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑞𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
160154, 159sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏𝑞) = ∅)
161 eqtr 2640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → (𝑎𝑞) = ∅)
162 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163162biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑎𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164161, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑎𝑞) = (𝑏𝑞) ∧ (𝑏𝑞) = ∅) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165164expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏𝑞) = ∅ → ((𝑎𝑞) = (𝑏𝑞) → ((𝑎𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166165com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝑞) = ∅ → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
167160, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
168167adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
169151, 168sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞𝐴) → ((𝑎𝑞) ∈ 𝐴 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
170150, 169syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞𝐴) → ((𝑎:𝑝𝐴𝑞𝑝) → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
171170exp4b 631 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞𝐴 → (𝑎:𝑝𝐴 → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))))
172171com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝𝐴 → (𝑏:𝑞𝐴 → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))))
173172imp32 449 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → ((𝑎𝑞) = (𝑏𝑞) → ∅ ∈ 𝐴)))
174149, 173syldd 72 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑞𝑝 → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → ∅ ∈ 𝐴)))
175174com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → (𝑞𝑝 → ∅ ∈ 𝐴)))
176175imp 445 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)) → (𝑞𝑝 → ∅ ∈ 𝐴))
177107, 176mtoi 190 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥)) → ¬ 𝑞𝑝)
178177ex 450 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑞𝑝))
179144, 178syld 47 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → ¬ 𝑞𝑝))
180140, 179jcad 555 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝)))
181 ordtri3or 5719 . . . . . . . . . . . . . . . . 17 ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
182115, 152, 181syl2an 494 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
183182adantr 481 . . . . . . . . . . . . . . 15 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑝𝑞𝑝 = 𝑞𝑞𝑝))
184 3orel13 31342 . . . . . . . . . . . . . . 15 ((¬ 𝑝𝑞 ∧ ¬ 𝑞𝑝) → ((𝑝𝑞𝑝 = 𝑞𝑞𝑝) → 𝑝 = 𝑞))
185180, 183, 184syl6ci 71 . . . . . . . . . . . . . 14 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑝 = 𝑞))
186185, 144jcad 555 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
187 ffn 6007 . . . . . . . . . . . . . . 15 (𝑎:𝑝𝐴𝑎 Fn 𝑝)
188 ffn 6007 . . . . . . . . . . . . . . 15 (𝑏:𝑞𝐴𝑏 Fn 𝑞)
189 eqfnfv2 6273 . . . . . . . . . . . . . . 15 ((𝑎 Fn 𝑝𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
190187, 188, 189syl2an 494 . . . . . . . . . . . . . 14 ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
191190adantl 482 . . . . . . . . . . . . 13 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥𝑝 (𝑎𝑥) = (𝑏𝑥))))
192186, 191sylibrd 249 . . . . . . . . . . . 12 (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝𝐴𝑏:𝑞𝐴)) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏))
193192ex 450 . . . . . . . . . . 11 ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝𝐴𝑏:𝑞𝐴) → (∀𝑥 ∈ On (𝑎𝑥) = (𝑏𝑥) → 𝑎 = 𝑏)))
194193rexlimivv 3030 . . . . . . . . . 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 393 . . . 4 ((𝑎𝐹𝑏𝐹) → ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201 3orcomb 1046 . . . . 5 ((𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏))
202 df-3or 1037 . . . . 5 ((𝑎𝑆𝑏𝑏𝑆𝑎𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203201, 202bitr2i 265 . . . 4 (((𝑎𝑆𝑏𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
204200, 203sylib 208 . . 3 ((𝑎𝐹𝑏𝐹) → (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎))
205204rgen2a 2972 . 2 𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)
206 df-so 5001 . 2 (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎𝐹𝑏𝐹 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)))
2076, 205, 206mpbir2an 954 1 𝑆 Or 𝐹
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3o 1035   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  [wsbc 3421  cun 3557  wss 3559  c0 3896  {csn 4153   class class class wbr 4618  {copab 4677   Po wpo 4998   Or wor 4999  dom cdm 5079  Ord word 5686  Oncon0 5687   Fn wfn 5847  wf 5848  cfv 5852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-fv 5860
This theorem is referenced by:  sltso  31564
  Copyright terms: Public domain W3C validator