Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  finminlem Structured version   Visualization version   GIF version

Theorem finminlem 34819
Description: A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009.)
Hypothesis
Ref Expression
finminlem.1 (π‘₯ = 𝑦 β†’ (πœ‘ ↔ πœ“))
Assertion
Ref Expression
finminlem (βˆƒπ‘₯ ∈ Fin πœ‘ β†’ βˆƒπ‘₯(πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦)))
Distinct variable groups:   πœ‘,𝑦   πœ“,π‘₯   π‘₯,𝑦
Allowed substitution hints:   πœ‘(π‘₯)   πœ“(𝑦)

Proof of Theorem finminlem
Dummy variables π‘˜ π‘š 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfe1 2148 . . . . 5 β„²π‘₯βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)
2 nfcv 2908 . . . . 5 β„²π‘₯Ο‰
31, 2nfrabw 3443 . . . 4 β„²π‘₯{𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)}
4 nfcv 2908 . . . 4 β„²π‘₯βˆ…
53, 4nfne 3046 . . 3 β„²π‘₯{𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…
6 isfi 8923 . . . 4 (π‘₯ ∈ Fin ↔ βˆƒπ‘š ∈ Ο‰ π‘₯ β‰ˆ π‘š)
7 19.8a 2175 . . . . . . . . . 10 ((π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘))
87anim2i 618 . . . . . . . . 9 ((π‘š ∈ Ο‰ ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (π‘š ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)))
983impb 1116 . . . . . . . 8 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ (π‘š ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)))
10 breq2 5114 . . . . . . . . . . 11 (𝑛 = π‘š β†’ (π‘₯ β‰ˆ 𝑛 ↔ π‘₯ β‰ˆ π‘š))
1110anbi1d 631 . . . . . . . . . 10 (𝑛 = π‘š β†’ ((π‘₯ β‰ˆ 𝑛 ∧ πœ‘) ↔ (π‘₯ β‰ˆ π‘š ∧ πœ‘)))
1211exbidv 1925 . . . . . . . . 9 (𝑛 = π‘š β†’ (βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘) ↔ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)))
1312elrab 3650 . . . . . . . 8 (π‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ↔ (π‘š ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)))
149, 13sylibr 233 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ π‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)})
1514ne0d 4300 . . . . . 6 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…)
16153exp 1120 . . . . 5 (π‘š ∈ Ο‰ β†’ (π‘₯ β‰ˆ π‘š β†’ (πœ‘ β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…)))
1716rexlimiv 3146 . . . 4 (βˆƒπ‘š ∈ Ο‰ π‘₯ β‰ˆ π‘š β†’ (πœ‘ β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…))
186, 17sylbi 216 . . 3 (π‘₯ ∈ Fin β†’ (πœ‘ β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…))
195, 18rexlimi 3245 . 2 (βˆƒπ‘₯ ∈ Fin πœ‘ β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…)
20 epweon 7714 . . 3 E We On
21 ssrab2 4042 . . . 4 {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} βŠ† Ο‰
22 omsson 7811 . . . 4 Ο‰ βŠ† On
2321, 22sstri 3958 . . 3 {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} βŠ† On
24 wefrc 5632 . . 3 (( E We On ∧ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} βŠ† On ∧ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…) β†’ βˆƒπ‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…)
2520, 23, 24mp3an12 1452 . 2 ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ… β†’ βˆƒπ‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…)
26 nfv 1918 . . . . . . 7 β„²π‘₯ π‘š ∈ Ο‰
27 nfcv 2908 . . . . . . . . 9 β„²π‘₯π‘š
283, 27nfin 4181 . . . . . . . 8 β„²π‘₯({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š)
2928nfeq1 2923 . . . . . . 7 β„²π‘₯({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…
3026, 29nfan 1903 . . . . . 6 β„²π‘₯(π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…)
31 simprr 772 . . . . . . . 8 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ πœ‘)
32 sspss 4064 . . . . . . . . . . . . 13 (𝑦 βŠ† π‘₯ ↔ (𝑦 ⊊ π‘₯ ∨ 𝑦 = π‘₯))
33 rspe 3235 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š) β†’ βˆƒπ‘š ∈ Ο‰ π‘₯ β‰ˆ π‘š)
34 pssss 4060 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ⊊ π‘₯ β†’ 𝑦 βŠ† π‘₯)
35 ssfi 9124 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘₯ ∈ Fin ∧ 𝑦 βŠ† π‘₯) β†’ 𝑦 ∈ Fin)
3634, 35sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘₯ ∈ Fin ∧ 𝑦 ⊊ π‘₯) β†’ 𝑦 ∈ Fin)
3736ex 414 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ Fin β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
386, 37sylbir 234 . . . . . . . . . . . . . . . . . . . . . . 23 (βˆƒπ‘š ∈ Ο‰ π‘₯ β‰ˆ π‘š β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
3933, 38syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š) β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
4039adantrr 716 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ Ο‰ ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
4140adantrr 716 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
42 isfi 8923 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ Fin ↔ βˆƒπ‘˜ ∈ Ο‰ 𝑦 β‰ˆ π‘˜)
43 simprll 778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ π‘˜ ∈ Ο‰)
44 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ 𝑦 β‰ˆ π‘˜)
45 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ πœ“)
46 vex 3452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑦 ∈ V
47 breq1 5113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘₯ = 𝑦 β†’ (π‘₯ β‰ˆ π‘˜ ↔ 𝑦 β‰ˆ π‘˜))
48 finminlem.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘₯ = 𝑦 β†’ (πœ‘ ↔ πœ“))
4947, 48anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ = 𝑦 β†’ ((π‘₯ β‰ˆ π‘˜ ∧ πœ‘) ↔ (𝑦 β‰ˆ π‘˜ ∧ πœ“)))
5046, 49spcev 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 β‰ˆ π‘˜ ∧ πœ“) β†’ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘))
5144, 45, 50syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘))
5233, 6sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š) β†’ π‘₯ ∈ Fin)
5352adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((π‘š ∈ Ο‰ ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ π‘₯ ∈ Fin)
5453adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ π‘₯ ∈ Fin)
5554adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ π‘₯ ∈ Fin)
56 php3 9163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘₯ ∈ Fin ∧ 𝑦 ⊊ π‘₯) β†’ 𝑦 β‰Ί π‘₯)
5756ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘₯ ∈ Fin β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 β‰Ί π‘₯))
5855, 57syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 β‰Ί π‘₯))
59 vex 3452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 π‘˜ ∈ V
60 ssdomg 8947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ ∈ V β†’ (π‘š βŠ† π‘˜ β†’ π‘š β‰Ό π‘˜))
6159, 60ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘š βŠ† π‘˜ β†’ π‘š β‰Ό π‘˜)
62 endomtr 8959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((π‘₯ β‰ˆ π‘š ∧ π‘š β‰Ό π‘˜) β†’ π‘₯ β‰Ό π‘˜)
6362ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (π‘₯ β‰ˆ π‘š β†’ (π‘š β‰Ό π‘˜ β†’ π‘₯ β‰Ό π‘˜))
6463ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“) β†’ (π‘š β‰Ό π‘˜ β†’ π‘₯ β‰Ό π‘˜))
6564ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (π‘š β‰Ό π‘˜ β†’ π‘₯ β‰Ό π‘˜))
66 ensym 8950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 β‰ˆ π‘˜ β†’ π‘˜ β‰ˆ 𝑦)
67 domentr 8960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((π‘₯ β‰Ό π‘˜ ∧ π‘˜ β‰ˆ 𝑦) β†’ π‘₯ β‰Ό 𝑦)
6866, 67sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((π‘₯ β‰Ό π‘˜ ∧ 𝑦 β‰ˆ π‘˜) β†’ π‘₯ β‰Ό 𝑦)
6968expcom 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 β‰ˆ π‘˜ β†’ (π‘₯ β‰Ό π‘˜ β†’ π‘₯ β‰Ό 𝑦))
7069ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (π‘₯ β‰Ό π‘˜ β†’ π‘₯ β‰Ό 𝑦))
7165, 70syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (π‘š β‰Ό π‘˜ β†’ π‘₯ β‰Ό 𝑦))
7261, 71syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (π‘š βŠ† π‘˜ β†’ π‘₯ β‰Ό 𝑦))
73 domnsym 9050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘₯ β‰Ό 𝑦 β†’ Β¬ 𝑦 β‰Ί π‘₯)
7473con2i 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 β‰Ί π‘₯ β†’ Β¬ π‘₯ β‰Ό 𝑦)
7572, 74nsyli 157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (𝑦 β‰Ί π‘₯ β†’ Β¬ π‘š βŠ† π‘˜))
7658, 75syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (𝑦 ⊊ π‘₯ β†’ Β¬ π‘š βŠ† π‘˜))
7776impr 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ Β¬ π‘š βŠ† π‘˜)
78 nnord 7815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘š ∈ Ο‰ β†’ Ord π‘š)
7978ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ Ord π‘š)
80 nnord 7815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ ∈ Ο‰ β†’ Ord π‘˜)
8180adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) β†’ Ord π‘˜)
8281ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ Ord π‘˜)
83 ordtri1 6355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Ord π‘š ∧ Ord π‘˜) β†’ (π‘š βŠ† π‘˜ ↔ Β¬ π‘˜ ∈ π‘š))
8483con2bid 355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Ord π‘š ∧ Ord π‘˜) β†’ (π‘˜ ∈ π‘š ↔ Β¬ π‘š βŠ† π‘˜))
8579, 82, 84syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ (π‘˜ ∈ π‘š ↔ Β¬ π‘š βŠ† π‘˜))
8677, 85mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ π‘˜ ∈ π‘š)
8743, 51, 86jca31 516 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ ((π‘˜ ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)) ∧ π‘˜ ∈ π‘š))
88 elin 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ ∈ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) ↔ (π‘˜ ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∧ π‘˜ ∈ π‘š))
89 breq2 5114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = π‘˜ β†’ (π‘₯ β‰ˆ 𝑛 ↔ π‘₯ β‰ˆ π‘˜))
9089anbi1d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = π‘˜ β†’ ((π‘₯ β‰ˆ 𝑛 ∧ πœ‘) ↔ (π‘₯ β‰ˆ π‘˜ ∧ πœ‘)))
9190exbidv 1925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = π‘˜ β†’ (βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘) ↔ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)))
9291elrab 3650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘˜ ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ↔ (π‘˜ ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)))
9392anbi1i 625 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘˜ ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∧ π‘˜ ∈ π‘š) ↔ ((π‘˜ ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)) ∧ π‘˜ ∈ π‘š))
9488, 93bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) ↔ ((π‘˜ ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)) ∧ π‘˜ ∈ π‘š))
9587, 94sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ π‘˜ ∈ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š))
9695ne0d 4300 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…)
9796exp44 439 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (π‘˜ ∈ Ο‰ β†’ (𝑦 β‰ˆ π‘˜ β†’ (𝑦 ⊊ π‘₯ β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…))))
9897rexlimdv 3151 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (βˆƒπ‘˜ ∈ Ο‰ 𝑦 β‰ˆ π‘˜ β†’ (𝑦 ⊊ π‘₯ β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…)))
9942, 98biimtrid 241 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ∈ Fin β†’ (𝑦 ⊊ π‘₯ β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…)))
10099com23 86 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ⊊ π‘₯ β†’ (𝑦 ∈ Fin β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…)))
10141, 100mpdd 43 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ⊊ π‘₯ β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…))
102101necon2bd 2960 . . . . . . . . . . . . . . . . . 18 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ Β¬ 𝑦 ⊊ π‘₯))
103102ex 414 . . . . . . . . . . . . . . . . 17 (π‘š ∈ Ο‰ β†’ (((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“) β†’ (({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ Β¬ 𝑦 ⊊ π‘₯)))
104103com23 86 . . . . . . . . . . . . . . . 16 (π‘š ∈ Ο‰ β†’ (({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ (((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“) β†’ Β¬ 𝑦 ⊊ π‘₯)))
105104imp31 419 . . . . . . . . . . . . . . 15 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ Β¬ 𝑦 ⊊ π‘₯)
106105pm2.21d 121 . . . . . . . . . . . . . 14 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ⊊ π‘₯ β†’ π‘₯ = 𝑦))
107 equcomi 2021 . . . . . . . . . . . . . . 15 (𝑦 = π‘₯ β†’ π‘₯ = 𝑦)
108107a1i 11 . . . . . . . . . . . . . 14 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 = π‘₯ β†’ π‘₯ = 𝑦))
109106, 108jaod 858 . . . . . . . . . . . . 13 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ ((𝑦 ⊊ π‘₯ ∨ 𝑦 = π‘₯) β†’ π‘₯ = 𝑦))
11032, 109biimtrid 241 . . . . . . . . . . . 12 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 βŠ† π‘₯ β†’ π‘₯ = 𝑦))
111110expr 458 . . . . . . . . . . 11 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (πœ“ β†’ (𝑦 βŠ† π‘₯ β†’ π‘₯ = 𝑦)))
112111com23 86 . . . . . . . . . 10 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (𝑦 βŠ† π‘₯ β†’ (πœ“ β†’ π‘₯ = 𝑦)))
113112impd 412 . . . . . . . . 9 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ ((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))
114113alrimiv 1931 . . . . . . . 8 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))
11531, 114jca 513 . . . . . . 7 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦)))
116115ex 414 . . . . . 6 ((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) β†’ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ (πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))))
11730, 116eximd 2210 . . . . 5 ((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) β†’ (βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ βˆƒπ‘₯(πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))))
118117impancom 453 . . . 4 ((π‘š ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ βˆƒπ‘₯(πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))))
11913, 118sylbi 216 . . 3 (π‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β†’ (({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ βˆƒπ‘₯(πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))))
120119rexlimiv 3146 . 2 (βˆƒπ‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ βˆƒπ‘₯(πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦)))
12119, 25, 1203syl 18 1 (βˆƒπ‘₯ ∈ Fin πœ‘ β†’ βˆƒπ‘₯(πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆƒwrex 3074  {crab 3410  Vcvv 3448   ∩ cin 3914   βŠ† wss 3915   ⊊ wpss 3916  βˆ…c0 4287   class class class wbr 5110   E cep 5541   We wwe 5592  Ord word 6321  Oncon0 6322  Ο‰com 7807   β‰ˆ cen 8887   β‰Ό cdom 8888   β‰Ί csdm 8889  Fincfn 8890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-om 7808  df-1o 8417  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator