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 35506
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 2145 . . . . 5 β„²π‘₯βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)
2 nfcv 2901 . . . . 5 β„²π‘₯Ο‰
31, 2nfrabw 3466 . . . 4 β„²π‘₯{𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)}
4 nfcv 2901 . . . 4 β„²π‘₯βˆ…
53, 4nfne 3041 . . 3 β„²π‘₯{𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…
6 isfi 8974 . . . 4 (π‘₯ ∈ Fin ↔ βˆƒπ‘š ∈ Ο‰ π‘₯ β‰ˆ π‘š)
7 19.8a 2172 . . . . . . . . . 10 ((π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘))
87anim2i 615 . . . . . . . . 9 ((π‘š ∈ Ο‰ ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (π‘š ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)))
983impb 1113 . . . . . . . 8 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ (π‘š ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)))
10 breq2 5151 . . . . . . . . . . 11 (𝑛 = π‘š β†’ (π‘₯ β‰ˆ 𝑛 ↔ π‘₯ β‰ˆ π‘š))
1110anbi1d 628 . . . . . . . . . 10 (𝑛 = π‘š β†’ ((π‘₯ β‰ˆ 𝑛 ∧ πœ‘) ↔ (π‘₯ β‰ˆ π‘š ∧ πœ‘)))
1211exbidv 1922 . . . . . . . . 9 (𝑛 = π‘š β†’ (βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘) ↔ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)))
1312elrab 3682 . . . . . . . 8 (π‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ↔ (π‘š ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘)))
149, 13sylibr 233 . . . . . . 7 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ π‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)})
1514ne0d 4334 . . . . . 6 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…)
16153exp 1117 . . . . 5 (π‘š ∈ Ο‰ β†’ (π‘₯ β‰ˆ π‘š β†’ (πœ‘ β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…)))
1716rexlimiv 3146 . . . 4 (βˆƒπ‘š ∈ Ο‰ π‘₯ β‰ˆ π‘š β†’ (πœ‘ β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…))
186, 17sylbi 216 . . 3 (π‘₯ ∈ Fin β†’ (πœ‘ β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…))
195, 18rexlimi 3254 . 2 (βˆƒπ‘₯ ∈ Fin πœ‘ β†’ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…)
20 epweon 7764 . . 3 E We On
21 ssrab2 4076 . . . 4 {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} βŠ† Ο‰
22 omsson 7861 . . . 4 Ο‰ βŠ† On
2321, 22sstri 3990 . . 3 {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} βŠ† On
24 wefrc 5669 . . 3 (( E We On ∧ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} βŠ† On ∧ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ…) β†’ βˆƒπ‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…)
2520, 23, 24mp3an12 1449 . 2 ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} β‰  βˆ… β†’ βˆƒπ‘š ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…)
26 nfv 1915 . . . . . . 7 β„²π‘₯ π‘š ∈ Ο‰
27 nfcv 2901 . . . . . . . . 9 β„²π‘₯π‘š
283, 27nfin 4215 . . . . . . . 8 β„²π‘₯({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š)
2928nfeq1 2916 . . . . . . 7 β„²π‘₯({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…
3026, 29nfan 1900 . . . . . 6 β„²π‘₯(π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…)
31 simprr 769 . . . . . . . 8 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ πœ‘)
32 sspss 4098 . . . . . . . . . . . . 13 (𝑦 βŠ† π‘₯ ↔ (𝑦 ⊊ π‘₯ ∨ 𝑦 = π‘₯))
33 rspe 3244 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š) β†’ βˆƒπ‘š ∈ Ο‰ π‘₯ β‰ˆ π‘š)
34 pssss 4094 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ⊊ π‘₯ β†’ 𝑦 βŠ† π‘₯)
35 ssfi 9175 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘₯ ∈ Fin ∧ 𝑦 βŠ† π‘₯) β†’ 𝑦 ∈ Fin)
3634, 35sylan2 591 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘₯ ∈ Fin ∧ 𝑦 ⊊ π‘₯) β†’ 𝑦 ∈ Fin)
3736ex 411 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ Fin β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
386, 37sylbir 234 . . . . . . . . . . . . . . . . . . . . . . 23 (βˆƒπ‘š ∈ Ο‰ π‘₯ β‰ˆ π‘š β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
3933, 38syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š) β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
4039adantrr 713 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ Ο‰ ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
4140adantrr 713 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 ∈ Fin))
42 isfi 8974 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ Fin ↔ βˆƒπ‘˜ ∈ Ο‰ 𝑦 β‰ˆ π‘˜)
43 simprll 775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ π‘˜ ∈ Ο‰)
44 simprlr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ 𝑦 β‰ˆ π‘˜)
45 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ πœ“)
46 vex 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑦 ∈ V
47 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘₯ = 𝑦 β†’ (π‘₯ β‰ˆ π‘˜ ↔ 𝑦 β‰ˆ π‘˜))
48 finminlem.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘₯ = 𝑦 β†’ (πœ‘ ↔ πœ“))
4947, 48anbi12d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ = 𝑦 β†’ ((π‘₯ β‰ˆ π‘˜ ∧ πœ‘) ↔ (𝑦 β‰ˆ π‘˜ ∧ πœ“)))
5046, 49spcev 3595 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 β‰ˆ π‘˜ ∧ πœ“) β†’ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘))
5144, 45, 50syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘))
5233, 6sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((π‘š ∈ Ο‰ ∧ π‘₯ β‰ˆ π‘š) β†’ π‘₯ ∈ Fin)
5352adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((π‘š ∈ Ο‰ ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ π‘₯ ∈ Fin)
5453adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ π‘₯ ∈ Fin)
5554adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ π‘₯ ∈ Fin)
56 php3 9214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘₯ ∈ Fin ∧ 𝑦 ⊊ π‘₯) β†’ 𝑦 β‰Ί π‘₯)
5756ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘₯ ∈ Fin β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 β‰Ί π‘₯))
5855, 57syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (𝑦 ⊊ π‘₯ β†’ 𝑦 β‰Ί π‘₯))
59 vex 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 π‘˜ ∈ V
60 ssdomg 8998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘˜ ∈ V β†’ (π‘š βŠ† π‘˜ β†’ π‘š β‰Ό π‘˜))
6159, 60ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘š βŠ† π‘˜ β†’ π‘š β‰Ό π‘˜)
62 endomtr 9010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((π‘₯ β‰ˆ π‘š ∧ π‘š β‰Ό π‘˜) β†’ π‘₯ β‰Ό π‘˜)
6362ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (π‘₯ β‰ˆ π‘š β†’ (π‘š β‰Ό π‘˜ β†’ π‘₯ β‰Ό π‘˜))
6463ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“) β†’ (π‘š β‰Ό π‘˜ β†’ π‘₯ β‰Ό π‘˜))
6564ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (π‘š β‰Ό π‘˜ β†’ π‘₯ β‰Ό π‘˜))
66 ensym 9001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 β‰ˆ π‘˜ β†’ π‘˜ β‰ˆ 𝑦)
67 domentr 9011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((π‘₯ β‰Ό π‘˜ ∧ π‘˜ β‰ˆ 𝑦) β†’ π‘₯ β‰Ό 𝑦)
6866, 67sylan2 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((π‘₯ β‰Ό π‘˜ ∧ 𝑦 β‰ˆ π‘˜) β†’ π‘₯ β‰Ό 𝑦)
6968expcom 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 β‰ˆ π‘˜ β†’ (π‘₯ β‰Ό π‘˜ β†’ π‘₯ β‰Ό 𝑦))
7069ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (π‘₯ β‰Ό π‘˜ β†’ π‘₯ β‰Ό 𝑦))
7165, 70syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (π‘š β‰Ό π‘˜ β†’ π‘₯ β‰Ό 𝑦))
7261, 71syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (π‘š βŠ† π‘˜ β†’ π‘₯ β‰Ό 𝑦))
73 domnsym 9101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘₯ β‰Ό 𝑦 β†’ Β¬ 𝑦 β‰Ί π‘₯)
7473con2i 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 β‰Ί π‘₯ β†’ Β¬ π‘₯ β‰Ό 𝑦)
7572, 74nsyli 157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (𝑦 β‰Ί π‘₯ β†’ Β¬ π‘š βŠ† π‘˜))
7658, 75syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜)) β†’ (𝑦 ⊊ π‘₯ β†’ Β¬ π‘š βŠ† π‘˜))
7776impr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ Β¬ π‘š βŠ† π‘˜)
78 nnord 7865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘š ∈ Ο‰ β†’ Ord π‘š)
7978ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ Ord π‘š)
80 nnord 7865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ ∈ Ο‰ β†’ Ord π‘˜)
8180adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) β†’ Ord π‘˜)
8281ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ Ord π‘˜)
83 ordtri1 6396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Ord π‘š ∧ Ord π‘˜) β†’ (π‘š βŠ† π‘˜ ↔ Β¬ π‘˜ ∈ π‘š))
8483con2bid 353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Ord π‘š ∧ Ord π‘˜) β†’ (π‘˜ ∈ π‘š ↔ Β¬ π‘š βŠ† π‘˜))
8579, 82, 84syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ (π‘˜ ∈ π‘š ↔ Β¬ π‘š βŠ† π‘˜))
8677, 85mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ π‘˜ ∈ π‘š)
8743, 51, 86jca31 513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ ((π‘˜ ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)) ∧ π‘˜ ∈ π‘š))
88 elin 3963 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ ∈ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) ↔ (π‘˜ ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∧ π‘˜ ∈ π‘š))
89 breq2 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = π‘˜ β†’ (π‘₯ β‰ˆ 𝑛 ↔ π‘₯ β‰ˆ π‘˜))
9089anbi1d 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = π‘˜ β†’ ((π‘₯ β‰ˆ 𝑛 ∧ πœ‘) ↔ (π‘₯ β‰ˆ π‘˜ ∧ πœ‘)))
9190exbidv 1922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = π‘˜ β†’ (βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘) ↔ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)))
9291elrab 3682 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘˜ ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ↔ (π‘˜ ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)))
9392anbi1i 622 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘˜ ∈ {𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∧ π‘˜ ∈ π‘š) ↔ ((π‘˜ ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)) ∧ π‘˜ ∈ π‘š))
9488, 93bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) ↔ ((π‘˜ ∈ Ο‰ ∧ βˆƒπ‘₯(π‘₯ β‰ˆ π‘˜ ∧ πœ‘)) ∧ π‘˜ ∈ π‘š))
9587, 94sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ π‘˜ ∈ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š))
9695ne0d 4334 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑦 β‰ˆ π‘˜) ∧ 𝑦 ⊊ π‘₯)) β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…)
9796exp44 436 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (π‘˜ ∈ Ο‰ β†’ (𝑦 β‰ˆ π‘˜ β†’ (𝑦 ⊊ π‘₯ β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…))))
9897rexlimdv 3151 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (βˆƒπ‘˜ ∈ Ο‰ 𝑦 β‰ˆ π‘˜ β†’ (𝑦 ⊊ π‘₯ β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…)))
9942, 98biimtrid 241 . . . . . . . . . . . . . . . . . . . . 21 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ∈ Fin β†’ (𝑦 ⊊ π‘₯ β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…)))
10099com23 86 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ⊊ π‘₯ β†’ (𝑦 ∈ Fin β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…)))
10141, 100mpdd 43 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ⊊ π‘₯ β†’ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) β‰  βˆ…))
102101necon2bd 2954 . . . . . . . . . . . . . . . . . 18 ((π‘š ∈ Ο‰ ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ Β¬ 𝑦 ⊊ π‘₯))
103102ex 411 . . . . . . . . . . . . . . . . 17 (π‘š ∈ Ο‰ β†’ (((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“) β†’ (({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ Β¬ 𝑦 ⊊ π‘₯)))
104103com23 86 . . . . . . . . . . . . . . . 16 (π‘š ∈ Ο‰ β†’ (({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ… β†’ (((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“) β†’ Β¬ 𝑦 ⊊ π‘₯)))
105104imp31 416 . . . . . . . . . . . . . . 15 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ Β¬ 𝑦 ⊊ π‘₯)
106105pm2.21d 121 . . . . . . . . . . . . . 14 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 ⊊ π‘₯ β†’ π‘₯ = 𝑦))
107 equcomi 2018 . . . . . . . . . . . . . . 15 (𝑦 = π‘₯ β†’ π‘₯ = 𝑦)
108107a1i 11 . . . . . . . . . . . . . 14 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 = π‘₯ β†’ π‘₯ = 𝑦))
109106, 108jaod 855 . . . . . . . . . . . . 13 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ ((𝑦 ⊊ π‘₯ ∨ 𝑦 = π‘₯) β†’ π‘₯ = 𝑦))
11032, 109biimtrid 241 . . . . . . . . . . . 12 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) ∧ πœ“)) β†’ (𝑦 βŠ† π‘₯ β†’ π‘₯ = 𝑦))
111110expr 455 . . . . . . . . . . 11 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (πœ“ β†’ (𝑦 βŠ† π‘₯ β†’ π‘₯ = 𝑦)))
112111com23 86 . . . . . . . . . 10 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (𝑦 βŠ† π‘₯ β†’ (πœ“ β†’ π‘₯ = 𝑦)))
113112impd 409 . . . . . . . . 9 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ ((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))
114113alrimiv 1928 . . . . . . . 8 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))
11531, 114jca 510 . . . . . . 7 (((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) ∧ (π‘₯ β‰ˆ π‘š ∧ πœ‘)) β†’ (πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦)))
116115ex 411 . . . . . 6 ((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) β†’ ((π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ (πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))))
11730, 116eximd 2207 . . . . 5 ((π‘š ∈ Ο‰ ∧ ({𝑛 ∈ Ο‰ ∣ βˆƒπ‘₯(π‘₯ β‰ˆ 𝑛 ∧ πœ‘)} ∩ π‘š) = βˆ…) β†’ (βˆƒπ‘₯(π‘₯ β‰ˆ π‘š ∧ πœ‘) β†’ βˆƒπ‘₯(πœ‘ ∧ βˆ€π‘¦((𝑦 βŠ† π‘₯ ∧ πœ“) β†’ π‘₯ = 𝑦))))
118117impancom 450 . . . 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 394   ∨ wo 843   ∧ w3a 1085  βˆ€wal 1537   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆƒwrex 3068  {crab 3430  Vcvv 3472   ∩ cin 3946   βŠ† wss 3947   ⊊ wpss 3948  βˆ…c0 4321   class class class wbr 5147   E cep 5578   We wwe 5629  Ord word 6362  Oncon0 6363  Ο‰com 7857   β‰ˆ cen 8938   β‰Ό cdom 8939   β‰Ί csdm 8940  Fincfn 8941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-om 7858  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator