MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pssnnOLD Structured version   Visualization version   GIF version

Theorem pssnnOLD 9267
Description: Obsolete version of pssnn 9170 as of 31-Jul-2024. (Contributed by NM, 22-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
pssnnOLD ((𝐴 ∈ Ο‰ ∧ 𝐡 ⊊ 𝐴) β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 β‰ˆ π‘₯)
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐡

Proof of Theorem pssnnOLD
Dummy variables 𝑦 𝑧 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pssss 4090 . . . 4 (𝐡 ⊊ 𝐴 β†’ 𝐡 βŠ† 𝐴)
2 ssexg 5316 . . . 4 ((𝐡 βŠ† 𝐴 ∧ 𝐴 ∈ Ο‰) β†’ 𝐡 ∈ V)
31, 2sylan 579 . . 3 ((𝐡 ⊊ 𝐴 ∧ 𝐴 ∈ Ο‰) β†’ 𝐡 ∈ V)
43ancoms 458 . 2 ((𝐴 ∈ Ο‰ ∧ 𝐡 ⊊ 𝐴) β†’ 𝐡 ∈ V)
5 psseq2 4083 . . . . . . . 8 (𝑧 = βˆ… β†’ (𝑀 ⊊ 𝑧 ↔ 𝑀 ⊊ βˆ…))
6 rexeq 3315 . . . . . . . 8 (𝑧 = βˆ… β†’ (βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯ ↔ βˆƒπ‘₯ ∈ βˆ… 𝑀 β‰ˆ π‘₯))
75, 6imbi12d 344 . . . . . . 7 (𝑧 = βˆ… β†’ ((𝑀 ⊊ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯) ↔ (𝑀 ⊊ βˆ… β†’ βˆƒπ‘₯ ∈ βˆ… 𝑀 β‰ˆ π‘₯)))
87albidv 1915 . . . . . 6 (𝑧 = βˆ… β†’ (βˆ€π‘€(𝑀 ⊊ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯) ↔ βˆ€π‘€(𝑀 ⊊ βˆ… β†’ βˆƒπ‘₯ ∈ βˆ… 𝑀 β‰ˆ π‘₯)))
9 psseq2 4083 . . . . . . . 8 (𝑧 = 𝑦 β†’ (𝑀 ⊊ 𝑧 ↔ 𝑀 ⊊ 𝑦))
10 rexeq 3315 . . . . . . . 8 (𝑧 = 𝑦 β†’ (βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯ ↔ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯))
119, 10imbi12d 344 . . . . . . 7 (𝑧 = 𝑦 β†’ ((𝑀 ⊊ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯) ↔ (𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)))
1211albidv 1915 . . . . . 6 (𝑧 = 𝑦 β†’ (βˆ€π‘€(𝑀 ⊊ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯) ↔ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)))
13 psseq2 4083 . . . . . . . 8 (𝑧 = suc 𝑦 β†’ (𝑀 ⊊ 𝑧 ↔ 𝑀 ⊊ suc 𝑦))
14 rexeq 3315 . . . . . . . 8 (𝑧 = suc 𝑦 β†’ (βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯ ↔ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))
1513, 14imbi12d 344 . . . . . . 7 (𝑧 = suc 𝑦 β†’ ((𝑀 ⊊ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯) ↔ (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)))
1615albidv 1915 . . . . . 6 (𝑧 = suc 𝑦 β†’ (βˆ€π‘€(𝑀 ⊊ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯) ↔ βˆ€π‘€(𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)))
17 psseq2 4083 . . . . . . . 8 (𝑧 = 𝐴 β†’ (𝑀 ⊊ 𝑧 ↔ 𝑀 ⊊ 𝐴))
18 rexeq 3315 . . . . . . . 8 (𝑧 = 𝐴 β†’ (βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯ ↔ βˆƒπ‘₯ ∈ 𝐴 𝑀 β‰ˆ π‘₯))
1917, 18imbi12d 344 . . . . . . 7 (𝑧 = 𝐴 β†’ ((𝑀 ⊊ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯) ↔ (𝑀 ⊊ 𝐴 β†’ βˆƒπ‘₯ ∈ 𝐴 𝑀 β‰ˆ π‘₯)))
2019albidv 1915 . . . . . 6 (𝑧 = 𝐴 β†’ (βˆ€π‘€(𝑀 ⊊ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝑧 𝑀 β‰ˆ π‘₯) ↔ βˆ€π‘€(𝑀 ⊊ 𝐴 β†’ βˆƒπ‘₯ ∈ 𝐴 𝑀 β‰ˆ π‘₯)))
21 npss0 4440 . . . . . . . 8 Β¬ 𝑀 ⊊ βˆ…
2221pm2.21i 119 . . . . . . 7 (𝑀 ⊊ βˆ… β†’ βˆƒπ‘₯ ∈ βˆ… 𝑀 β‰ˆ π‘₯)
2322ax-gen 1789 . . . . . 6 βˆ€π‘€(𝑀 ⊊ βˆ… β†’ βˆƒπ‘₯ ∈ βˆ… 𝑀 β‰ˆ π‘₯)
24 nfv 1909 . . . . . . 7 Ⅎ𝑀 𝑦 ∈ Ο‰
25 nfa1 2140 . . . . . . 7 β„²π‘€βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)
26 elequ1 2105 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 β†’ (𝑧 ∈ 𝑀 ↔ 𝑦 ∈ 𝑀))
2726biimpcd 248 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ 𝑀 β†’ (𝑧 = 𝑦 β†’ 𝑦 ∈ 𝑀))
2827con3d 152 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ 𝑀 β†’ (Β¬ 𝑦 ∈ 𝑀 β†’ Β¬ 𝑧 = 𝑦))
2928adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑀) β†’ (Β¬ 𝑦 ∈ 𝑀 β†’ Β¬ 𝑧 = 𝑦))
30 pssss 4090 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ⊊ suc 𝑦 β†’ 𝑀 βŠ† suc 𝑦)
3130sseld 3976 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ⊊ suc 𝑦 β†’ (𝑧 ∈ 𝑀 β†’ 𝑧 ∈ suc 𝑦))
32 elsuci 6425 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ suc 𝑦 β†’ (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦))
3332ord 861 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ suc 𝑦 β†’ (Β¬ 𝑧 ∈ 𝑦 β†’ 𝑧 = 𝑦))
3433con1d 145 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ suc 𝑦 β†’ (Β¬ 𝑧 = 𝑦 β†’ 𝑧 ∈ 𝑦))
3531, 34syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ⊊ suc 𝑦 β†’ (𝑧 ∈ 𝑀 β†’ (Β¬ 𝑧 = 𝑦 β†’ 𝑧 ∈ 𝑦)))
3635imp 406 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑀) β†’ (Β¬ 𝑧 = 𝑦 β†’ 𝑧 ∈ 𝑦))
3729, 36syld 47 . . . . . . . . . . . . . . . . . 18 ((𝑀 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑀) β†’ (Β¬ 𝑦 ∈ 𝑀 β†’ 𝑧 ∈ 𝑦))
3837impancom 451 . . . . . . . . . . . . . . . . 17 ((𝑀 ⊊ suc 𝑦 ∧ Β¬ 𝑦 ∈ 𝑀) β†’ (𝑧 ∈ 𝑀 β†’ 𝑧 ∈ 𝑦))
3938ssrdv 3983 . . . . . . . . . . . . . . . 16 ((𝑀 ⊊ suc 𝑦 ∧ Β¬ 𝑦 ∈ 𝑀) β†’ 𝑀 βŠ† 𝑦)
4039anim1i 614 . . . . . . . . . . . . . . 15 (((𝑀 ⊊ suc 𝑦 ∧ Β¬ 𝑦 ∈ 𝑀) ∧ Β¬ 𝑀 = 𝑦) β†’ (𝑀 βŠ† 𝑦 ∧ Β¬ 𝑀 = 𝑦))
41 dfpss2 4080 . . . . . . . . . . . . . . 15 (𝑀 ⊊ 𝑦 ↔ (𝑀 βŠ† 𝑦 ∧ Β¬ 𝑀 = 𝑦))
4240, 41sylibr 233 . . . . . . . . . . . . . 14 (((𝑀 ⊊ suc 𝑦 ∧ Β¬ 𝑦 ∈ 𝑀) ∧ Β¬ 𝑀 = 𝑦) β†’ 𝑀 ⊊ 𝑦)
43 elelsuc 6431 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝑦 β†’ π‘₯ ∈ suc 𝑦)
4443anim1i 614 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝑦 ∧ 𝑀 β‰ˆ π‘₯) β†’ (π‘₯ ∈ suc 𝑦 ∧ 𝑀 β‰ˆ π‘₯))
4544reximi2 3073 . . . . . . . . . . . . . 14 (βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯ β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)
4642, 45imim12i 62 . . . . . . . . . . . . 13 ((𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯) β†’ (((𝑀 ⊊ suc 𝑦 ∧ Β¬ 𝑦 ∈ 𝑀) ∧ Β¬ 𝑀 = 𝑦) β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))
4746exp4c 432 . . . . . . . . . . . 12 ((𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯) β†’ (𝑀 ⊊ suc 𝑦 β†’ (Β¬ 𝑦 ∈ 𝑀 β†’ (Β¬ 𝑀 = 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))))
4847sps 2170 . . . . . . . . . . 11 (βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯) β†’ (𝑀 ⊊ suc 𝑦 β†’ (Β¬ 𝑦 ∈ 𝑀 β†’ (Β¬ 𝑀 = 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))))
4948adantl 481 . . . . . . . . . 10 ((𝑦 ∈ Ο‰ ∧ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)) β†’ (𝑀 ⊊ suc 𝑦 β†’ (Β¬ 𝑦 ∈ 𝑀 β†’ (Β¬ 𝑀 = 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))))
5049com4t 93 . . . . . . . . 9 (Β¬ 𝑦 ∈ 𝑀 β†’ (Β¬ 𝑀 = 𝑦 β†’ ((𝑦 ∈ Ο‰ ∧ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)) β†’ (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))))
51 anidm 564 . . . . . . . . . . . . . 14 ((𝑀 ⊊ suc 𝑦 ∧ 𝑀 ⊊ suc 𝑦) ↔ 𝑀 ⊊ suc 𝑦)
52 ssdif 4134 . . . . . . . . . . . . . . . . 17 (𝑀 βŠ† suc 𝑦 β†’ (𝑀 βˆ– {𝑦}) βŠ† (suc 𝑦 βˆ– {𝑦}))
53 nnord 7860 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ Ο‰ β†’ Ord 𝑦)
54 orddif 6454 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 β†’ 𝑦 = (suc 𝑦 βˆ– {𝑦}))
5553, 54syl 17 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ Ο‰ β†’ 𝑦 = (suc 𝑦 βˆ– {𝑦}))
5655sseq2d 4009 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ Ο‰ β†’ ((𝑀 βˆ– {𝑦}) βŠ† 𝑦 ↔ (𝑀 βˆ– {𝑦}) βŠ† (suc 𝑦 βˆ– {𝑦})))
5752, 56imbitrrid 245 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Ο‰ β†’ (𝑀 βŠ† suc 𝑦 β†’ (𝑀 βˆ– {𝑦}) βŠ† 𝑦))
5830, 57syl5 34 . . . . . . . . . . . . . . 15 (𝑦 ∈ Ο‰ β†’ (𝑀 ⊊ suc 𝑦 β†’ (𝑀 βˆ– {𝑦}) βŠ† 𝑦))
59 pssnel 4465 . . . . . . . . . . . . . . . 16 (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘§(𝑧 ∈ suc 𝑦 ∧ Β¬ 𝑧 ∈ 𝑀))
60 eleq2 2816 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 βˆ– {𝑦}) = 𝑦 β†’ (𝑧 ∈ (𝑀 βˆ– {𝑦}) ↔ 𝑧 ∈ 𝑦))
61 eldifi 4121 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝑀 βˆ– {𝑦}) β†’ 𝑧 ∈ 𝑀)
6260, 61syl6bir 254 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 βˆ– {𝑦}) = 𝑦 β†’ (𝑧 ∈ 𝑦 β†’ 𝑧 ∈ 𝑀))
6362adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑀 βˆ– {𝑦}) = 𝑦) β†’ (𝑧 ∈ 𝑦 β†’ 𝑧 ∈ 𝑀))
64 eleq1a 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ 𝑀 β†’ (𝑧 = 𝑦 β†’ 𝑧 ∈ 𝑀))
6533, 64sylan9r 508 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ suc 𝑦) β†’ (Β¬ 𝑧 ∈ 𝑦 β†’ 𝑧 ∈ 𝑀))
6665adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑀 βˆ– {𝑦}) = 𝑦) β†’ (Β¬ 𝑧 ∈ 𝑦 β†’ 𝑧 ∈ 𝑀))
6763, 66pm2.61d 179 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑀 βˆ– {𝑦}) = 𝑦) β†’ 𝑧 ∈ 𝑀)
6867ex 412 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ suc 𝑦) β†’ ((𝑀 βˆ– {𝑦}) = 𝑦 β†’ 𝑧 ∈ 𝑀))
6968con3d 152 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ suc 𝑦) β†’ (Β¬ 𝑧 ∈ 𝑀 β†’ Β¬ (𝑀 βˆ– {𝑦}) = 𝑦))
7069expimpd 453 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝑀 β†’ ((𝑧 ∈ suc 𝑦 ∧ Β¬ 𝑧 ∈ 𝑀) β†’ Β¬ (𝑀 βˆ– {𝑦}) = 𝑦))
7170exlimdv 1928 . . . . . . . . . . . . . . . 16 (𝑦 ∈ 𝑀 β†’ (βˆƒπ‘§(𝑧 ∈ suc 𝑦 ∧ Β¬ 𝑧 ∈ 𝑀) β†’ Β¬ (𝑀 βˆ– {𝑦}) = 𝑦))
7259, 71syl5 34 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝑀 β†’ (𝑀 ⊊ suc 𝑦 β†’ Β¬ (𝑀 βˆ– {𝑦}) = 𝑦))
7358, 72im2anan9r 620 . . . . . . . . . . . . . 14 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ ((𝑀 ⊊ suc 𝑦 ∧ 𝑀 ⊊ suc 𝑦) β†’ ((𝑀 βˆ– {𝑦}) βŠ† 𝑦 ∧ Β¬ (𝑀 βˆ– {𝑦}) = 𝑦)))
7451, 73biimtrrid 242 . . . . . . . . . . . . 13 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ (𝑀 ⊊ suc 𝑦 β†’ ((𝑀 βˆ– {𝑦}) βŠ† 𝑦 ∧ Β¬ (𝑀 βˆ– {𝑦}) = 𝑦)))
75 dfpss2 4080 . . . . . . . . . . . . 13 ((𝑀 βˆ– {𝑦}) ⊊ 𝑦 ↔ ((𝑀 βˆ– {𝑦}) βŠ† 𝑦 ∧ Β¬ (𝑀 βˆ– {𝑦}) = 𝑦))
7674, 75imbitrrdi 251 . . . . . . . . . . . 12 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ (𝑀 ⊊ suc 𝑦 β†’ (𝑀 βˆ– {𝑦}) ⊊ 𝑦))
77 psseq1 4082 . . . . . . . . . . . . . . 15 (𝑀 = 𝑧 β†’ (𝑀 ⊊ 𝑦 ↔ 𝑧 ⊊ 𝑦))
78 breq1 5144 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑧 β†’ (𝑀 β‰ˆ π‘₯ ↔ 𝑧 β‰ˆ π‘₯))
7978rexbidv 3172 . . . . . . . . . . . . . . 15 (𝑀 = 𝑧 β†’ (βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯ ↔ βˆƒπ‘₯ ∈ 𝑦 𝑧 β‰ˆ π‘₯))
8077, 79imbi12d 344 . . . . . . . . . . . . . 14 (𝑀 = 𝑧 β†’ ((𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯) ↔ (𝑧 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑧 β‰ˆ π‘₯)))
8180cbvalvw 2031 . . . . . . . . . . . . 13 (βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯) ↔ βˆ€π‘§(𝑧 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑧 β‰ˆ π‘₯))
82 vex 3472 . . . . . . . . . . . . . . 15 𝑀 ∈ V
8382difexi 5321 . . . . . . . . . . . . . 14 (𝑀 βˆ– {𝑦}) ∈ V
84 psseq1 4082 . . . . . . . . . . . . . . 15 (𝑧 = (𝑀 βˆ– {𝑦}) β†’ (𝑧 ⊊ 𝑦 ↔ (𝑀 βˆ– {𝑦}) ⊊ 𝑦))
85 breq1 5144 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑀 βˆ– {𝑦}) β†’ (𝑧 β‰ˆ π‘₯ ↔ (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯))
8685rexbidv 3172 . . . . . . . . . . . . . . 15 (𝑧 = (𝑀 βˆ– {𝑦}) β†’ (βˆƒπ‘₯ ∈ 𝑦 𝑧 β‰ˆ π‘₯ ↔ βˆƒπ‘₯ ∈ 𝑦 (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯))
8784, 86imbi12d 344 . . . . . . . . . . . . . 14 (𝑧 = (𝑀 βˆ– {𝑦}) β†’ ((𝑧 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑧 β‰ˆ π‘₯) ↔ ((𝑀 βˆ– {𝑦}) ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯)))
8883, 87spcv 3589 . . . . . . . . . . . . 13 (βˆ€π‘§(𝑧 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑧 β‰ˆ π‘₯) β†’ ((𝑀 βˆ– {𝑦}) ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯))
8981, 88sylbi 216 . . . . . . . . . . . 12 (βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯) β†’ ((𝑀 βˆ– {𝑦}) ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯))
9076, 89sylan9 507 . . . . . . . . . . 11 (((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) ∧ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)) β†’ (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯))
91 ordsucelsuc 7807 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝑦 β†’ (π‘₯ ∈ 𝑦 ↔ suc π‘₯ ∈ suc 𝑦))
9291biimpd 228 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑦 β†’ (π‘₯ ∈ 𝑦 β†’ suc π‘₯ ∈ suc 𝑦))
9353, 92syl 17 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ Ο‰ β†’ (π‘₯ ∈ 𝑦 β†’ suc π‘₯ ∈ suc 𝑦))
9493adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ (π‘₯ ∈ 𝑦 β†’ suc π‘₯ ∈ suc 𝑦))
9594adantrd 491 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ ((π‘₯ ∈ 𝑦 ∧ (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯) β†’ suc π‘₯ ∈ suc 𝑦))
96 elnn 7863 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ 𝑦 ∧ 𝑦 ∈ Ο‰) β†’ π‘₯ ∈ Ο‰)
97 snex 5424 . . . . . . . . . . . . . . . . . . . . . . . 24 {βŸ¨π‘¦, π‘₯⟩} ∈ V
98 vex 3472 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 ∈ V
99 vex 3472 . . . . . . . . . . . . . . . . . . . . . . . . 25 π‘₯ ∈ V
10098, 99f1osn 6867 . . . . . . . . . . . . . . . . . . . . . . . 24 {βŸ¨π‘¦, π‘₯⟩}:{𝑦}–1-1-ontoβ†’{π‘₯}
101 f1oen3g 8964 . . . . . . . . . . . . . . . . . . . . . . . 24 (({βŸ¨π‘¦, π‘₯⟩} ∈ V ∧ {βŸ¨π‘¦, π‘₯⟩}:{𝑦}–1-1-ontoβ†’{π‘₯}) β†’ {𝑦} β‰ˆ {π‘₯})
10297, 100, 101mp2an 689 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑦} β‰ˆ {π‘₯}
103102jctr 524 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ β†’ ((𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ ∧ {𝑦} β‰ˆ {π‘₯}))
104 nnord 7860 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ Ο‰ β†’ Ord π‘₯)
105 orddisj 6396 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord π‘₯ β†’ (π‘₯ ∩ {π‘₯}) = βˆ…)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ ∈ Ο‰ β†’ (π‘₯ ∩ {π‘₯}) = βˆ…)
107 incom 4196 . . . . . . . . . . . . . . . . . . . . . . . 24 ({𝑦} ∩ (𝑀 βˆ– {𝑦})) = ((𝑀 βˆ– {𝑦}) ∩ {𝑦})
108 disjdif 4466 . . . . . . . . . . . . . . . . . . . . . . . 24 ({𝑦} ∩ (𝑀 βˆ– {𝑦})) = βˆ…
109107, 108eqtr3i 2756 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 βˆ– {𝑦}) ∩ {𝑦}) = βˆ…
110106, 109jctil 519 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ Ο‰ β†’ (((𝑀 βˆ– {𝑦}) ∩ {𝑦}) = βˆ… ∧ (π‘₯ ∩ {π‘₯}) = βˆ…))
111 unen 9048 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ ∧ {𝑦} β‰ˆ {π‘₯}) ∧ (((𝑀 βˆ– {𝑦}) ∩ {𝑦}) = βˆ… ∧ (π‘₯ ∩ {π‘₯}) = βˆ…)) β†’ ((𝑀 βˆ– {𝑦}) βˆͺ {𝑦}) β‰ˆ (π‘₯ βˆͺ {π‘₯}))
112103, 110, 111syl2an 595 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ ∧ π‘₯ ∈ Ο‰) β†’ ((𝑀 βˆ– {𝑦}) βˆͺ {𝑦}) β‰ˆ (π‘₯ βˆͺ {π‘₯}))
113 difsnid 4808 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ 𝑀 β†’ ((𝑀 βˆ– {𝑦}) βˆͺ {𝑦}) = 𝑀)
114113eqcomd 2732 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ 𝑀 β†’ 𝑀 = ((𝑀 βˆ– {𝑦}) βˆͺ {𝑦}))
115 df-suc 6364 . . . . . . . . . . . . . . . . . . . . . . 23 suc π‘₯ = (π‘₯ βˆͺ {π‘₯})
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ 𝑀 β†’ suc π‘₯ = (π‘₯ βˆͺ {π‘₯}))
117114, 116breq12d 5154 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ 𝑀 β†’ (𝑀 β‰ˆ suc π‘₯ ↔ ((𝑀 βˆ– {𝑦}) βˆͺ {𝑦}) β‰ˆ (π‘₯ βˆͺ {π‘₯})))
118112, 117imbitrrid 245 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ 𝑀 β†’ (((𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ ∧ π‘₯ ∈ Ο‰) β†’ 𝑀 β‰ˆ suc π‘₯))
11996, 118sylan2i 605 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ 𝑀 β†’ (((𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ ∧ (π‘₯ ∈ 𝑦 ∧ 𝑦 ∈ Ο‰)) β†’ 𝑀 β‰ˆ suc π‘₯))
120119exp4d 433 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ 𝑀 β†’ ((𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ β†’ (π‘₯ ∈ 𝑦 β†’ (𝑦 ∈ Ο‰ β†’ 𝑀 β‰ˆ suc π‘₯))))
121120com24 95 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝑀 β†’ (𝑦 ∈ Ο‰ β†’ (π‘₯ ∈ 𝑦 β†’ ((𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ β†’ 𝑀 β‰ˆ suc π‘₯))))
122121imp4b 421 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ ((π‘₯ ∈ 𝑦 ∧ (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯) β†’ 𝑀 β‰ˆ suc π‘₯))
12395, 122jcad 512 . . . . . . . . . . . . . . 15 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ ((π‘₯ ∈ 𝑦 ∧ (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯) β†’ (suc π‘₯ ∈ suc 𝑦 ∧ 𝑀 β‰ˆ suc π‘₯)))
124 breq2 5145 . . . . . . . . . . . . . . . 16 (𝑧 = suc π‘₯ β†’ (𝑀 β‰ˆ 𝑧 ↔ 𝑀 β‰ˆ suc π‘₯))
125124rspcev 3606 . . . . . . . . . . . . . . 15 ((suc π‘₯ ∈ suc 𝑦 ∧ 𝑀 β‰ˆ suc π‘₯) β†’ βˆƒπ‘§ ∈ suc 𝑦𝑀 β‰ˆ 𝑧)
126123, 125syl6 35 . . . . . . . . . . . . . 14 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ ((π‘₯ ∈ 𝑦 ∧ (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯) β†’ βˆƒπ‘§ ∈ suc 𝑦𝑀 β‰ˆ 𝑧))
127126exlimdv 1928 . . . . . . . . . . . . 13 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ (βˆƒπ‘₯(π‘₯ ∈ 𝑦 ∧ (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯) β†’ βˆƒπ‘§ ∈ suc 𝑦𝑀 β‰ˆ 𝑧))
128 df-rex 3065 . . . . . . . . . . . . 13 (βˆƒπ‘₯ ∈ 𝑦 (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ ↔ βˆƒπ‘₯(π‘₯ ∈ 𝑦 ∧ (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯))
129 breq2 5145 . . . . . . . . . . . . . 14 (π‘₯ = 𝑧 β†’ (𝑀 β‰ˆ π‘₯ ↔ 𝑀 β‰ˆ 𝑧))
130129cbvrexvw 3229 . . . . . . . . . . . . 13 (βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯ ↔ βˆƒπ‘§ ∈ suc 𝑦𝑀 β‰ˆ 𝑧)
131127, 128, 1303imtr4g 296 . . . . . . . . . . . 12 ((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) β†’ (βˆƒπ‘₯ ∈ 𝑦 (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))
132131adantr 480 . . . . . . . . . . 11 (((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) ∧ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)) β†’ (βˆƒπ‘₯ ∈ 𝑦 (𝑀 βˆ– {𝑦}) β‰ˆ π‘₯ β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))
13390, 132syld 47 . . . . . . . . . 10 (((𝑦 ∈ 𝑀 ∧ 𝑦 ∈ Ο‰) ∧ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)) β†’ (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))
134133expl 457 . . . . . . . . 9 (𝑦 ∈ 𝑀 β†’ ((𝑦 ∈ Ο‰ ∧ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)) β†’ (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)))
13582eqelsuc 6442 . . . . . . . . . . 11 (𝑀 = 𝑦 β†’ 𝑀 ∈ suc 𝑦)
13682enref 8983 . . . . . . . . . . 11 𝑀 β‰ˆ 𝑀
137 breq2 5145 . . . . . . . . . . . 12 (π‘₯ = 𝑀 β†’ (𝑀 β‰ˆ π‘₯ ↔ 𝑀 β‰ˆ 𝑀))
138137rspcev 3606 . . . . . . . . . . 11 ((𝑀 ∈ suc 𝑦 ∧ 𝑀 β‰ˆ 𝑀) β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)
139135, 136, 138sylancl 585 . . . . . . . . . 10 (𝑀 = 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)
1401392a1d 26 . . . . . . . . 9 (𝑀 = 𝑦 β†’ ((𝑦 ∈ Ο‰ ∧ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)) β†’ (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)))
14150, 134, 140pm2.61ii 183 . . . . . . . 8 ((𝑦 ∈ Ο‰ ∧ βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯)) β†’ (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯))
142141ex 412 . . . . . . 7 (𝑦 ∈ Ο‰ β†’ (βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯) β†’ (𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)))
14324, 25, 142alrimd 2200 . . . . . 6 (𝑦 ∈ Ο‰ β†’ (βˆ€π‘€(𝑀 ⊊ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝑦 𝑀 β‰ˆ π‘₯) β†’ βˆ€π‘€(𝑀 ⊊ suc 𝑦 β†’ βˆƒπ‘₯ ∈ suc 𝑦𝑀 β‰ˆ π‘₯)))
1448, 12, 16, 20, 23, 143finds 7886 . . . . 5 (𝐴 ∈ Ο‰ β†’ βˆ€π‘€(𝑀 ⊊ 𝐴 β†’ βˆƒπ‘₯ ∈ 𝐴 𝑀 β‰ˆ π‘₯))
145 psseq1 4082 . . . . . . 7 (𝑀 = 𝐡 β†’ (𝑀 ⊊ 𝐴 ↔ 𝐡 ⊊ 𝐴))
146 breq1 5144 . . . . . . . 8 (𝑀 = 𝐡 β†’ (𝑀 β‰ˆ π‘₯ ↔ 𝐡 β‰ˆ π‘₯))
147146rexbidv 3172 . . . . . . 7 (𝑀 = 𝐡 β†’ (βˆƒπ‘₯ ∈ 𝐴 𝑀 β‰ˆ π‘₯ ↔ βˆƒπ‘₯ ∈ 𝐴 𝐡 β‰ˆ π‘₯))
148145, 147imbi12d 344 . . . . . 6 (𝑀 = 𝐡 β†’ ((𝑀 ⊊ 𝐴 β†’ βˆƒπ‘₯ ∈ 𝐴 𝑀 β‰ˆ π‘₯) ↔ (𝐡 ⊊ 𝐴 β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 β‰ˆ π‘₯)))
149148spcgv 3580 . . . . 5 (𝐡 ∈ V β†’ (βˆ€π‘€(𝑀 ⊊ 𝐴 β†’ βˆƒπ‘₯ ∈ 𝐴 𝑀 β‰ˆ π‘₯) β†’ (𝐡 ⊊ 𝐴 β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 β‰ˆ π‘₯)))
150144, 149syl5 34 . . . 4 (𝐡 ∈ V β†’ (𝐴 ∈ Ο‰ β†’ (𝐡 ⊊ 𝐴 β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 β‰ˆ π‘₯)))
151150com3l 89 . . 3 (𝐴 ∈ Ο‰ β†’ (𝐡 ⊊ 𝐴 β†’ (𝐡 ∈ V β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 β‰ˆ π‘₯)))
152151imp 406 . 2 ((𝐴 ∈ Ο‰ ∧ 𝐡 ⊊ 𝐴) β†’ (𝐡 ∈ V β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 β‰ˆ π‘₯))
1534, 152mpd 15 1 ((𝐴 ∈ Ο‰ ∧ 𝐡 ⊊ 𝐴) β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 β‰ˆ π‘₯)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395  βˆ€wal 1531   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  βˆƒwrex 3064  Vcvv 3468   βˆ– cdif 3940   βˆͺ cun 3941   ∩ cin 3942   βŠ† wss 3943   ⊊ wpss 3944  βˆ…c0 4317  {csn 4623  βŸ¨cop 4629   class class class wbr 5141  Ord word 6357  suc csuc 6360  β€“1-1-ontoβ†’wf1o 6536  Ο‰com 7852   β‰ˆ cen 8938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-om 7853  df-en 8942
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator