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

Theorem isfin2-2 9933
Description: FinII expressed in terms of minimal elements. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Proof shortened by Mario Carneiro, 16-May-2015.)
Assertion
Ref Expression
isfin2-2 (𝐴𝑉 → (𝐴 ∈ FinII ↔ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦)))
Distinct variable group:   𝑦,𝐴
Allowed substitution hint:   𝑉(𝑦)

Proof of Theorem isfin2-2
Dummy variables 𝑏 𝑐 𝑚 𝑛 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elpwi 4522 . . . 4 (𝑦 ∈ 𝒫 𝒫 𝐴𝑦 ⊆ 𝒫 𝐴)
2 fin2i2 9932 . . . . 5 (((𝐴 ∈ FinII𝑦 ⊆ 𝒫 𝐴) ∧ (𝑦 ≠ ∅ ∧ [] Or 𝑦)) → 𝑦𝑦)
32ex 416 . . . 4 ((𝐴 ∈ FinII𝑦 ⊆ 𝒫 𝐴) → ((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦))
41, 3sylan2 596 . . 3 ((𝐴 ∈ FinII𝑦 ∈ 𝒫 𝒫 𝐴) → ((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦))
54ralrimiva 3105 . 2 (𝐴 ∈ FinII → ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦))
6 elpwi 4522 . . . . 5 (𝑏 ∈ 𝒫 𝒫 𝐴𝑏 ⊆ 𝒫 𝐴)
7 simp1r 1200 . . . . . . . 8 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → 𝑏 ⊆ 𝒫 𝐴)
8 simp1l 1199 . . . . . . . . . . 11 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → 𝐴𝑉)
9 simp3l 1203 . . . . . . . . . . 11 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → 𝑏 ≠ ∅)
10 fin23lem7 9930 . . . . . . . . . . 11 ((𝐴𝑉𝑏 ⊆ 𝒫 𝐴𝑏 ≠ ∅) → {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ≠ ∅)
118, 7, 9, 10syl3anc 1373 . . . . . . . . . 10 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ≠ ∅)
12 sorpsscmpl 7522 . . . . . . . . . . . 12 ( [] Or 𝑏 → [] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏})
1312adantl 485 . . . . . . . . . . 11 ((𝑏 ≠ ∅ ∧ [] Or 𝑏) → [] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏})
14133ad2ant3 1137 . . . . . . . . . 10 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → [] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏})
15 neeq1 3003 . . . . . . . . . . . . 13 (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} → (𝑦 ≠ ∅ ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ≠ ∅))
16 soeq2 5490 . . . . . . . . . . . . 13 (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} → ( [] Or 𝑦 ↔ [] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}))
1715, 16anbi12d 634 . . . . . . . . . . . 12 (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} → ((𝑦 ≠ ∅ ∧ [] Or 𝑦) ↔ ({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ≠ ∅ ∧ [] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏})))
18 inteq 4862 . . . . . . . . . . . . 13 (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} → 𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏})
19 id 22 . . . . . . . . . . . . 13 (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} → 𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏})
2018, 19eleq12d 2832 . . . . . . . . . . . 12 (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} → ( 𝑦𝑦 {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}))
2117, 20imbi12d 348 . . . . . . . . . . 11 (𝑦 = {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} → (((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ↔ (({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ≠ ∅ ∧ [] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}) → {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏})))
22 simp2 1139 . . . . . . . . . . 11 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦))
23 ssrab2 3993 . . . . . . . . . . . 12 {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴
24 pwexg 5271 . . . . . . . . . . . . 13 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
25 elpw2g 5237 . . . . . . . . . . . . 13 (𝒫 𝐴 ∈ V → ({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴 ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴))
268, 24, 253syl 18 . . . . . . . . . . . 12 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → ({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴 ↔ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ⊆ 𝒫 𝐴))
2723, 26mpbiri 261 . . . . . . . . . . 11 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ 𝒫 𝒫 𝐴)
2821, 22, 27rspcdva 3539 . . . . . . . . . 10 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → (({𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ≠ ∅ ∧ [] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}) → {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}))
2911, 14, 28mp2and 699 . . . . . . . . 9 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏})
30 sorpssint 7521 . . . . . . . . . 10 ( [] Or {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} → (∃𝑧 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ¬ 𝑤𝑧 {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}))
3114, 30syl 17 . . . . . . . . 9 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → (∃𝑧 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ¬ 𝑤𝑧 {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}))
3229, 31mpbird 260 . . . . . . . 8 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → ∃𝑧 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ¬ 𝑤𝑧)
33 psseq1 4002 . . . . . . . . 9 (𝑚 = (𝐴𝑧) → (𝑚𝑛 ↔ (𝐴𝑧) ⊊ 𝑛))
34 psseq1 4002 . . . . . . . . 9 (𝑤 = (𝐴𝑛) → (𝑤𝑧 ↔ (𝐴𝑛) ⊊ 𝑧))
35 pssdifcom1 4401 . . . . . . . . 9 ((𝑧𝐴𝑛𝐴) → ((𝐴𝑧) ⊊ 𝑛 ↔ (𝐴𝑛) ⊊ 𝑧))
3633, 34, 35fin23lem11 9931 . . . . . . . 8 (𝑏 ⊆ 𝒫 𝐴 → (∃𝑧 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴𝑐) ∈ 𝑏} ¬ 𝑤𝑧 → ∃𝑚𝑏𝑛𝑏 ¬ 𝑚𝑛))
377, 32, 36sylc 65 . . . . . . 7 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → ∃𝑚𝑏𝑛𝑏 ¬ 𝑚𝑛)
38 simp3r 1204 . . . . . . . 8 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → [] Or 𝑏)
39 sorpssuni 7520 . . . . . . . 8 ( [] Or 𝑏 → (∃𝑚𝑏𝑛𝑏 ¬ 𝑚𝑛 𝑏𝑏))
4038, 39syl 17 . . . . . . 7 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → (∃𝑚𝑏𝑛𝑏 ¬ 𝑚𝑛 𝑏𝑏))
4137, 40mpbid 235 . . . . . 6 (((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) ∧ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) ∧ (𝑏 ≠ ∅ ∧ [] Or 𝑏)) → 𝑏𝑏)
42413exp 1121 . . . . 5 ((𝐴𝑉𝑏 ⊆ 𝒫 𝐴) → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) → ((𝑏 ≠ ∅ ∧ [] Or 𝑏) → 𝑏𝑏)))
436, 42sylan2 596 . . . 4 ((𝐴𝑉𝑏 ∈ 𝒫 𝒫 𝐴) → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) → ((𝑏 ≠ ∅ ∧ [] Or 𝑏) → 𝑏𝑏)))
4443ralrimdva 3110 . . 3 (𝐴𝑉 → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) → ∀𝑏 ∈ 𝒫 𝒫 𝐴((𝑏 ≠ ∅ ∧ [] Or 𝑏) → 𝑏𝑏)))
45 isfin2 9908 . . 3 (𝐴𝑉 → (𝐴 ∈ FinII ↔ ∀𝑏 ∈ 𝒫 𝒫 𝐴((𝑏 ≠ ∅ ∧ [] Or 𝑏) → 𝑏𝑏)))
4644, 45sylibrd 262 . 2 (𝐴𝑉 → (∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦) → 𝐴 ∈ FinII))
475, 46impbid2 229 1 (𝐴𝑉 → (𝐴 ∈ FinII ↔ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [] Or 𝑦) → 𝑦𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  {crab 3065  Vcvv 3408  cdif 3863  wss 3866  wpss 3867  c0 4237  𝒫 cpw 4513   cuni 4819   cint 4859   Or wor 5467   [] crpss 7510  FinIIcfin2 9893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-int 4860  df-br 5054  df-opab 5116  df-po 5468  df-so 5469  df-xp 5557  df-rel 5558  df-rpss 7511  df-fin2 9900
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator