Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ordtconlem1 Structured version   Visualization version   GIF version

Theorem ordtconlem1 29298
 Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtcon 29299. See also reconnlem1 22437. (Contributed by Thierry Arnoux, 14-Sep-2018.)
Hypotheses
Ref Expression
ordtcon.x 𝐵 = (Base‘𝐾)
ordtcon.l = ((le‘𝐾) ∩ (𝐵 × 𝐵))
ordtcon.j 𝐽 = (ordTop‘ )
Assertion
Ref Expression
ordtconlem1 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → ((𝐽t 𝐴) ∈ Con → ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)))
Distinct variable groups:   𝑥,𝑟,𝑦,𝐴   𝐵,𝑟,𝑥,𝑦   𝐽,𝑟   𝐾,𝑟,𝑥,𝑦   𝑥, ,𝑦
Allowed substitution hints:   𝐽(𝑥,𝑦)   (𝑟)

Proof of Theorem ordtconlem1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfv 1830 . . . . 5 𝑟(𝐾 ∈ Toset ∧ 𝐴𝐵)
2 nfcv 2751 . . . . . . 7 𝑟𝐴
3 nfra2 2930 . . . . . . 7 𝑟𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
42, 3nfral 2929 . . . . . 6 𝑟𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
54nfn 1768 . . . . 5 𝑟 ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)
61, 5nfan 1816 . . . 4 𝑟((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
7 tospos 28989 . . . . . . . . . 10 (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8 posprs 16772 . . . . . . . . . 10 (𝐾 ∈ Poset → 𝐾 ∈ Preset )
9 ordtcon.j . . . . . . . . . . 11 𝐽 = (ordTop‘ )
10 ordtcon.l . . . . . . . . . . . . . 14 = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11 fvex 6113 . . . . . . . . . . . . . . 15 (le‘𝐾) ∈ V
1211inex1 4727 . . . . . . . . . . . . . 14 ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
1310, 12eqeltri 2684 . . . . . . . . . . . . 13 ∈ V
14 eqid 2610 . . . . . . . . . . . . . 14 dom = dom
1514ordttopon 20807 . . . . . . . . . . . . 13 ( ∈ V → (ordTop‘ ) ∈ (TopOn‘dom ))
1613, 15ax-mp 5 . . . . . . . . . . . 12 (ordTop‘ ) ∈ (TopOn‘dom )
17 ordtcon.x . . . . . . . . . . . . . 14 𝐵 = (Base‘𝐾)
1817, 10prsdm 29288 . . . . . . . . . . . . 13 (𝐾 ∈ Preset → dom = 𝐵)
1918fveq2d 6107 . . . . . . . . . . . 12 (𝐾 ∈ Preset → (TopOn‘dom ) = (TopOn‘𝐵))
2016, 19syl5eleq 2694 . . . . . . . . . . 11 (𝐾 ∈ Preset → (ordTop‘ ) ∈ (TopOn‘𝐵))
219, 20syl5eqel 2692 . . . . . . . . . 10 (𝐾 ∈ Preset → 𝐽 ∈ (TopOn‘𝐵))
227, 8, 213syl 18 . . . . . . . . 9 (𝐾 ∈ Toset → 𝐽 ∈ (TopOn‘𝐵))
2322ad3antrrr 762 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐽 ∈ (TopOn‘𝐵))
2423adantlr 747 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐽 ∈ (TopOn‘𝐵))
25 simpllr 795 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴𝐵)
2625adantlr 747 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴𝐵)
27 simpll 786 . . . . . . . . . . . 12 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → 𝐾 ∈ Toset)
2827, 7, 83syl 18 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → 𝐾 ∈ Preset )
29 snex 4835 . . . . . . . . . . . . . . . 16 {𝐵} ∈ V
30 fvex 6113 . . . . . . . . . . . . . . . . . . . 20 (Base‘𝐾) ∈ V
3117, 30eqeltri 2684 . . . . . . . . . . . . . . . . . . 19 𝐵 ∈ V
3231mptex 6390 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3332rnex 6992 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∈ V
3431mptex 6390 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3534rnex 6992 . . . . . . . . . . . . . . . . 17 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ∈ V
3633, 35unex 6854 . . . . . . . . . . . . . . . 16 (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ∈ V
3729, 36unex 6854 . . . . . . . . . . . . . . 15 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V
38 ssfii 8208 . . . . . . . . . . . . . . 15 (({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
3937, 38ax-mp 5 . . . . . . . . . . . . . 14 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))
40 fvex 6113 . . . . . . . . . . . . . . 15 (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ∈ V
41 bastg 20581 . . . . . . . . . . . . . . 15 ((fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ∈ V → (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
4240, 41ax-mp 5 . . . . . . . . . . . . . 14 (fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
4339, 42sstri 3577 . . . . . . . . . . . . 13 ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})))))
44 eqid 2610 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
45 eqid 2610 . . . . . . . . . . . . . . 15 ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
4617, 10, 44, 45ordtprsval 29292 . . . . . . . . . . . . . 14 (𝐾 ∈ Preset → (ordTop‘ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
479, 46syl5eq 2656 . . . . . . . . . . . . 13 (𝐾 ∈ Preset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))))))
4843, 47syl5sseqr 3617 . . . . . . . . . . . 12 (𝐾 ∈ Preset → ({𝐵} ∪ (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))) ⊆ 𝐽)
4948unssbd 3753 . . . . . . . . . . 11 (𝐾 ∈ Preset → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
5028, 49syl 17 . . . . . . . . . 10 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ∪ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})) ⊆ 𝐽)
5150unssbd 3753 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ⊆ 𝐽)
52 breq2 4587 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑟 𝑧𝑟 𝑦))
5352notbid 307 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑦))
5453cbvrabv 3172 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}
55 breq1 4586 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑟 → (𝑥 𝑦𝑟 𝑦))
5655notbid 307 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (¬ 𝑥 𝑦 ↔ ¬ 𝑟 𝑦))
5756rabbidv 3164 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑥 𝑦} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦})
5857eqeq2d 2620 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦} ↔ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}))
5958rspcev 3282 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑟 𝑦}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6054, 59mpan2 703 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6131rabex 4740 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V
62 eqid 2610 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6362elrnmpt 5293 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6461, 63ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑟 𝑧} = {𝑦𝐵 ∣ ¬ 𝑥 𝑦})
6560, 64sylibr 223 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6665adantl 481 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑥 𝑦}))
6751, 66sseldd 3569 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6867ad2antrr 758 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∈ 𝐽)
6950unssad 3752 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ⊆ 𝐽)
70 breq1 4586 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 𝑟𝑦 𝑟))
7170notbid 307 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ 𝑧 𝑟 ↔ ¬ 𝑦 𝑟))
7271cbvrabv 3172 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}
73 breq2 4587 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑟 → (𝑦 𝑥𝑦 𝑟))
7473notbid 307 . . . . . . . . . . . . . . 15 (𝑥 = 𝑟 → (¬ 𝑦 𝑥 ↔ ¬ 𝑦 𝑟))
7574rabbidv 3164 . . . . . . . . . . . . . 14 (𝑥 = 𝑟 → {𝑦𝐵 ∣ ¬ 𝑦 𝑥} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟})
7675eqeq2d 2620 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥} ↔ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}))
7776rspcev 3282 . . . . . . . . . . . 12 ((𝑟𝐵 ∧ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑟}) → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7872, 77mpan2 703 . . . . . . . . . . 11 (𝑟𝐵 → ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
7931rabex 4740 . . . . . . . . . . . 12 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V
80 eqid 2610 . . . . . . . . . . . . 13 (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) = (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
8180elrnmpt 5293 . . . . . . . . . . . 12 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ V → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8279, 81ax-mp 5 . . . . . . . . . . 11 ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}) ↔ ∃𝑥𝐵 {𝑧𝐵 ∣ ¬ 𝑧 𝑟} = {𝑦𝐵 ∣ ¬ 𝑦 𝑥})
8378, 82sylibr 223 . . . . . . . . . 10 (𝑟𝐵 → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8483adantl 481 . . . . . . . . 9 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ ran (𝑥𝐵 ↦ {𝑦𝐵 ∣ ¬ 𝑦 𝑥}))
8569, 84sseldd 3569 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
8685ad2antrr 758 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∈ 𝐽)
87 simpll 786 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵))
88 simpr 476 . . . . . . . . 9 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
8987, 88jca 553 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴))
90 simplrl 796 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑥𝐴 ¬ 𝑟 𝑥)
91 ssel 3562 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
9291ancrd 575 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑥𝐴 → (𝑥𝐵𝑥𝐴)))
9392anim1d 586 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥)))
9493impl 648 . . . . . . . . . . . 12 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
95 elin 3758 . . . . . . . . . . . . 13 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴))
96 breq2 4587 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → (𝑟 𝑧𝑟 𝑥))
9796notbid 307 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (¬ 𝑟 𝑧 ↔ ¬ 𝑟 𝑥))
9897elrab 3331 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑥𝐵 ∧ ¬ 𝑟 𝑥))
9998anbi1i 727 . . . . . . . . . . . . 13 ((𝑥 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑥𝐴) ↔ ((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴))
100 an32 835 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ¬ 𝑟 𝑥) ∧ 𝑥𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
10195, 99, 1003bitri 285 . . . . . . . . . . . 12 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ↔ ((𝑥𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥))
10294, 101sylibr 223 . . . . . . . . . . 11 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → 𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴))
103 ne0i 3880 . . . . . . . . . . 11 (𝑥 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
104102, 103syl 17 . . . . . . . . . 10 (((𝐴𝐵𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10525, 104sylanl1 680 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) ∧ ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
106105r19.29an 3059 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑥𝐴 ¬ 𝑟 𝑥) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
10789, 90, 106syl2anc 691 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ 𝐴) ≠ ∅)
108 simplrr 797 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ∃𝑦𝐴 ¬ 𝑦 𝑟)
109 ssel 3562 . . . . . . . . . . . . . . 15 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
110109ancrd 575 . . . . . . . . . . . . . 14 (𝐴𝐵 → (𝑦𝐴 → (𝑦𝐵𝑦𝐴)))
111110anim1d 586 . . . . . . . . . . . . 13 (𝐴𝐵 → ((𝑦𝐴 ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟)))
112111impl 648 . . . . . . . . . . . 12 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
113 elin 3758 . . . . . . . . . . . . 13 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴))
11471elrab 3331 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑦𝐵 ∧ ¬ 𝑦 𝑟))
115114anbi1i 727 . . . . . . . . . . . . 13 ((𝑦 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∧ 𝑦𝐴) ↔ ((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴))
116 an32 835 . . . . . . . . . . . . 13 (((𝑦𝐵 ∧ ¬ 𝑦 𝑟) ∧ 𝑦𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
117113, 115, 1163bitri 285 . . . . . . . . . . . 12 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ↔ ((𝑦𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟))
118112, 117sylibr 223 . . . . . . . . . . 11 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → 𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴))
119 ne0i 3880 . . . . . . . . . . 11 (𝑦 ∈ ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
120118, 119syl 17 . . . . . . . . . 10 (((𝐴𝐵𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
12125, 120sylanl1 680 . . . . . . . . 9 ((((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) ∧ ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
122121r19.29an 3059 . . . . . . . 8 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
12389, 108, 122syl2anc 691 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑧 𝑟} ∩ 𝐴) ≠ ∅)
12417, 10trleile 28997 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → (𝑟 𝑧𝑧 𝑟))
125 oran 516 . . . . . . . . . . . . . . . 16 ((𝑟 𝑧𝑧 𝑟) ↔ ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
126124, 125sylib 207 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
1271263expa 1257 . . . . . . . . . . . . . 14 (((𝐾 ∈ Toset ∧ 𝑟𝐵) ∧ 𝑧𝐵) → ¬ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
128127nrexdv 2984 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
129 rabid 3095 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ↔ (𝑧𝐵 ∧ ¬ 𝑟 𝑧))
130 rabid 3095 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟} ↔ (𝑧𝐵 ∧ ¬ 𝑧 𝑟))
131129, 130anbi12i 729 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
132 elin 3758 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∧ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
133 anandi 867 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∧ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
134131, 132, 1333bitr4i 291 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
135134exbii 1764 . . . . . . . . . . . . . . 15 (∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
136 nfrab1 3099 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑟 𝑧}
137 nfrab1 3099 . . . . . . . . . . . . . . . . 17 𝑧{𝑧𝐵 ∣ ¬ 𝑧 𝑟}
138136, 137nfin 3782 . . . . . . . . . . . . . . . 16 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
139138n0f 3886 . . . . . . . . . . . . . . 15 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
140 df-rex 2902 . . . . . . . . . . . . . . 15 (∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ∃𝑧(𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∧ ¬ 𝑧 𝑟)))
141135, 139, 1403bitr4i 291 . . . . . . . . . . . . . 14 (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ≠ ∅ ↔ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟))
142141necon1bbii 2831 . . . . . . . . . . . . 13 (¬ ∃𝑧𝐵𝑟 𝑧 ∧ ¬ 𝑧 𝑟) ↔ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
143128, 142sylib 207 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
144143adantlr 747 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
145144adantr 480 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = ∅)
146145ineq1d 3775 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
147 0in 3921 . . . . . . . . 9 (∅ ∩ 𝐴) = ∅
148146, 147syl6eq 2660 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
149148adantlr 747 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → (({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∩ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ∩ 𝐴) = ∅)
150 simplr 788 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝑟𝐵)
151 simpr 476 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ¬ 𝑟𝐴)
152 vex 3176 . . . . . . . . . . . . . . 15 𝑟 ∈ V
153152snss 4259 . . . . . . . . . . . . . 14 (𝑟𝐵 ↔ {𝑟} ⊆ 𝐵)
154 eldif 3550 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ (𝑟𝐵 ∧ ¬ 𝑟𝐴))
155152snss 4259 . . . . . . . . . . . . . . . 16 (𝑟 ∈ (𝐵𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
156154, 155bitr3i 265 . . . . . . . . . . . . . . 15 ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ {𝑟} ⊆ (𝐵𝐴))
157 ssconb 3705 . . . . . . . . . . . . . . 15 (({𝑟} ⊆ 𝐵𝐴𝐵) → ({𝑟} ⊆ (𝐵𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
158156, 157syl5bb 271 . . . . . . . . . . . . . 14 (({𝑟} ⊆ 𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
159153, 158sylanb 488 . . . . . . . . . . . . 13 ((𝑟𝐵𝐴𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
160159adantl 481 . . . . . . . . . . . 12 ((𝐾 ∈ Toset ∧ (𝑟𝐵𝐴𝐵)) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
161160anass1rs 845 . . . . . . . . . . 11 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
162161adantr 480 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((𝑟𝐵 ∧ ¬ 𝑟𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
163150, 151, 162mpbi2and 958 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
1647ad3antrrr 762 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐾 ∈ Poset)
165 nfv 1830 . . . . . . . . . . 11 𝑧(𝐾 ∈ Poset ∧ 𝑟𝐵)
166136, 137nfun 3731 . . . . . . . . . . 11 𝑧({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟})
167 nfcv 2751 . . . . . . . . . . 11 𝑧(𝐵 ∖ {𝑟})
168 ianor 508 . . . . . . . . . . . . . . 15 (¬ (𝑟 𝑧𝑧 𝑟) ↔ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟))
16917, 10posrasymb 28988 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑟 = 𝑧))
170 equcom 1932 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑧𝑧 = 𝑟)
171169, 170syl6bb 275 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((𝑟 𝑧𝑧 𝑟) ↔ 𝑧 = 𝑟))
172171necon3bbid 2819 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → (¬ (𝑟 𝑧𝑧 𝑟) ↔ 𝑧𝑟))
173168, 172syl5bbr 273 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑧𝐵) → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟))
1741733expia 1259 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧𝐵 → ((¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟) ↔ 𝑧𝑟)))
175174pm5.32d 669 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ (𝑧𝐵𝑧𝑟)))
176129, 130orbi12i 542 . . . . . . . . . . . . 13 ((𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
177 elun 3715 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ (𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∨ 𝑧 ∈ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
178 andi 907 . . . . . . . . . . . . 13 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ ((𝑧𝐵 ∧ ¬ 𝑟 𝑧) ∨ (𝑧𝐵 ∧ ¬ 𝑧 𝑟)))
179176, 177, 1783bitr4ri 292 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (¬ 𝑟 𝑧 ∨ ¬ 𝑧 𝑟)) ↔ 𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
180 eldifsn 4260 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧𝐵𝑧𝑟))
181180bicomi 213 . . . . . . . . . . . 12 ((𝑧𝐵𝑧𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
182175, 179, 1813bitr3g 301 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → (𝑧 ∈ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
183165, 166, 167, 182eqrd 3586 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ 𝑟𝐵) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
184164, 150, 183syl2anc 691 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}) = (𝐵 ∖ {𝑟}))
185163, 184sseqtr4d 3605 . . . . . . . 8 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
186185adantlr 747 . . . . . . 7 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → 𝐴 ⊆ ({𝑧𝐵 ∣ ¬ 𝑟 𝑧} ∪ {𝑧𝐵 ∣ ¬ 𝑧 𝑟}))
18724, 26, 68, 86, 107, 123, 149, 186nconsubb 21036 . . . . . 6 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)) ∧ ¬ 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Con)
188187anasss 677 . . . . 5 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Con)
189188adantllr 751 . . . 4 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) ∧ 𝑟𝐵) ∧ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Con)
190 rexanali 2981 . . . . . . . . . . 11 (∃𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
191190rexbii 3023 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
192 rexcom 3080 . . . . . . . . . 10 (∃𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
193 rexnal 2978 . . . . . . . . . 10 (∃𝑦𝐴 ¬ ∀𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
194191, 192, 1933bitr3i 289 . . . . . . . . 9 (∃𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
195194rexbii 3023 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
196 rexcom 3080 . . . . . . . 8 (∃𝑥𝐴𝑟𝐵𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
197 rexnal 2978 . . . . . . . 8 (∃𝑥𝐴 ¬ ∀𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
198195, 196, 1973bitr3i 289 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴))
199 r19.41v 3070 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
200199rexbii 3023 . . . . . . . . 9 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
201 r19.41v 3070 . . . . . . . . 9 (∃𝑥𝐴 (∃𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴))
202 reeanv 3086 . . . . . . . . . 10 (∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ↔ (∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦))
203202anbi1i 727 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 (𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
204200, 201, 2033bitri 285 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
205204rexbii 3023 . . . . . . 7 (∃𝑟𝐵𝑥𝐴𝑦𝐴 ((𝑥 𝑟𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
206198, 205bitr3i 265 . . . . . 6 (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴))
20727ad2antrr 758 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Toset)
20825sselda 3568 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐵)
209 simpllr 795 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑟𝐵)
21017, 10trleile 28997 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑥𝐵𝑟𝐵) → (𝑥 𝑟𝑟 𝑥))
211207, 208, 209, 210syl3anc 1318 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟𝑟 𝑥))
212 simpr 476 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝐴)
213 simplr 788 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ 𝑟𝐴)
214 nelne2 2879 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ¬ 𝑟𝐴) → 𝑥𝑟)
215212, 213, 214syl2anc 691 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝑥𝑟)
216164adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → 𝐾 ∈ Poset)
21717, 10posrasymb 28988 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → ((𝑥 𝑟𝑟 𝑥) ↔ 𝑥 = 𝑟))
218217necon3bbid 2819 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑥𝐵𝑟𝐵) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
219216, 208, 209, 218syl3anc 1318 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (¬ (𝑥 𝑟𝑟 𝑥) ↔ 𝑥𝑟))
220215, 219mpbird 246 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ¬ (𝑥 𝑟𝑟 𝑥))
221211, 220jca 553 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → ((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)))
222 pm5.17 928 . . . . . . . . . . . 12 (((𝑥 𝑟𝑟 𝑥) ∧ ¬ (𝑥 𝑟𝑟 𝑥)) ↔ (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
223221, 222sylib 207 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑥𝐴) → (𝑥 𝑟 ↔ ¬ 𝑟 𝑥))
224223rexbidva 3031 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑥𝐴 𝑥 𝑟 ↔ ∃𝑥𝐴 ¬ 𝑟 𝑥))
22527ad2antrr 758 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Toset)
226 simpllr 795 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝐵)
22725sselda 3568 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐵)
22817, 10trleile 28997 . . . . . . . . . . . . . 14 ((𝐾 ∈ Toset ∧ 𝑟𝐵𝑦𝐵) → (𝑟 𝑦𝑦 𝑟))
229225, 226, 227, 228syl3anc 1318 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦𝑦 𝑟))
230 simpr 476 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝐴)
231 simplr 788 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ 𝑟𝐴)
232 nelne2 2879 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ¬ 𝑟𝐴) → 𝑦𝑟)
233230, 231, 232syl2anc 691 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑦𝑟)
234233necomd 2837 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝑟𝑦)
235164adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → 𝐾 ∈ Poset)
23617, 10posrasymb 28988 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → ((𝑟 𝑦𝑦 𝑟) ↔ 𝑟 = 𝑦))
237236necon3bbid 2819 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ 𝑟𝐵𝑦𝐵) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
238235, 226, 227, 237syl3anc 1318 . . . . . . . . . . . . . 14 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (¬ (𝑟 𝑦𝑦 𝑟) ↔ 𝑟𝑦))
239234, 238mpbird 246 . . . . . . . . . . . . 13 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ¬ (𝑟 𝑦𝑦 𝑟))
240229, 239jca 553 . . . . . . . . . . . 12 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → ((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)))
241 pm5.17 928 . . . . . . . . . . . 12 (((𝑟 𝑦𝑦 𝑟) ∧ ¬ (𝑟 𝑦𝑦 𝑟)) ↔ (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
242240, 241sylib 207 . . . . . . . . . . 11 (((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) ∧ 𝑦𝐴) → (𝑟 𝑦 ↔ ¬ 𝑦 𝑟))
243242rexbidva 3031 . . . . . . . . . 10 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → (∃𝑦𝐴 𝑟 𝑦 ↔ ∃𝑦𝐴 ¬ 𝑦 𝑟))
244224, 243anbi12d 743 . . . . . . . . 9 ((((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) ∧ ¬ 𝑟𝐴) → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟)))
245244ex 449 . . . . . . . 8 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (¬ 𝑟𝐴 → ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ↔ (∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟))))
246245pm5.32rd 670 . . . . . . 7 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ 𝑟𝐵) → (((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
247246rexbidva 3031 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (∃𝑟𝐵 ((∃𝑥𝐴 𝑥 𝑟 ∧ ∃𝑦𝐴 𝑟 𝑦) ∧ ¬ 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
248206, 247syl5bb 271 . . . . 5 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) ↔ ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴)))
249248biimpa 500 . . . 4 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ∃𝑟𝐵 ((∃𝑥𝐴 ¬ 𝑟 𝑥 ∧ ∃𝑦𝐴 ¬ 𝑦 𝑟) ∧ ¬ 𝑟𝐴))
2506, 189, 249r19.29af 3058 . . 3 (((𝐾 ∈ Toset ∧ 𝐴𝐵) ∧ ¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)) → ¬ (𝐽t 𝐴) ∈ Con)
251250ex 449 . 2 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → (¬ ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴) → ¬ (𝐽t 𝐴) ∈ Con))
252251con4d 113 1 ((𝐾 ∈ Toset ∧ 𝐴𝐵) → ((𝐽t 𝐴) ∈ Con → ∀𝑥𝐴𝑦𝐴𝑟𝐵 ((𝑥 𝑟𝑟 𝑦) → 𝑟𝐴)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  dom cdm 5038  ran crn 5039  ‘cfv 5804  (class class class)co 6549  ficfi 8199  Basecbs 15695  lecple 15775   ↾t crest 15904  topGenctg 15921  ordTopcordt 15982   Preset cpreset 16749  Posetcpo 16763  Tosetctos 16856  TopOnctopon 20518  Conccon 21024 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-rep 4699  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-reu 2903  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-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  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-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-fin 7845  df-fi 8200  df-rest 15906  df-topgen 15927  df-ordt 15984  df-preset 16751  df-poset 16769  df-toset 16857  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-con 21025 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator