Metamath Proof Explorer


Theorem isfin2-2

Description: Fin2 expressed in terms of minimal elements. (Contributed by Stefan O'Rear, 2-Nov-2014) (Proof shortened by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion isfin2-2 ( 𝐴𝑉 → ( 𝐴 ∈ FinII ↔ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 elpwi ( 𝑦 ∈ 𝒫 𝒫 𝐴𝑦 ⊆ 𝒫 𝐴 )
2 fin2i2 ( ( ( 𝐴 ∈ FinII𝑦 ⊆ 𝒫 𝐴 ) ∧ ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) ) → 𝑦𝑦 )
3 2 ex ( ( 𝐴 ∈ FinII𝑦 ⊆ 𝒫 𝐴 ) → ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) )
4 1 3 sylan2 ( ( 𝐴 ∈ FinII𝑦 ∈ 𝒫 𝒫 𝐴 ) → ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) )
5 4 ralrimiva ( 𝐴 ∈ FinII → ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) )
6 elpwi ( 𝑏 ∈ 𝒫 𝒫 𝐴𝑏 ⊆ 𝒫 𝐴 )
7 simp1r ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → 𝑏 ⊆ 𝒫 𝐴 )
8 simp1l ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → 𝐴𝑉 )
9 simp3l ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → 𝑏 ≠ ∅ )
10 fin23lem7 ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴𝑏 ≠ ∅ ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ≠ ∅ )
11 8 7 9 10 syl3anc ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ≠ ∅ )
12 sorpsscmpl ( [] Or 𝑏 → [] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } )
13 12 adantl ( ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) → [] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } )
14 13 3ad2ant3 ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → [] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } )
15 neeq1 ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } → ( 𝑦 ≠ ∅ ↔ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ≠ ∅ ) )
16 soeq2 ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } → ( [] Or 𝑦 ↔ [] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) )
17 15 16 anbi12d ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } → ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) ↔ ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ≠ ∅ ∧ [] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) ) )
18 inteq ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } → 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } )
19 id ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } → 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } )
20 18 19 eleq12d ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } → ( 𝑦𝑦 { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) )
21 17 20 imbi12d ( 𝑦 = { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } → ( ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ↔ ( ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ≠ ∅ ∧ [] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) ) )
22 simp2 ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) )
23 ssrab2 { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ⊆ 𝒫 𝐴
24 pwexg ( 𝐴𝑉 → 𝒫 𝐴 ∈ V )
25 elpw2g ( 𝒫 𝐴 ∈ V → ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ 𝒫 𝒫 𝐴 ↔ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ⊆ 𝒫 𝐴 ) )
26 8 24 25 3syl ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ 𝒫 𝒫 𝐴 ↔ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ⊆ 𝒫 𝐴 ) )
27 23 26 mpbiri ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ 𝒫 𝒫 𝐴 )
28 21 22 27 rspcdva ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → ( ( { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ≠ ∅ ∧ [] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) )
29 11 14 28 mp2and ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } )
30 sorpssint ( [] Or { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } → ( ∃ 𝑧 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ¬ 𝑤𝑧 { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) )
31 14 30 syl ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → ( ∃ 𝑧 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ¬ 𝑤𝑧 { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ) )
32 29 31 mpbird ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → ∃ 𝑧 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ¬ 𝑤𝑧 )
33 psseq1 ( 𝑚 = ( 𝐴𝑧 ) → ( 𝑚𝑛 ↔ ( 𝐴𝑧 ) ⊊ 𝑛 ) )
34 psseq1 ( 𝑤 = ( 𝐴𝑛 ) → ( 𝑤𝑧 ↔ ( 𝐴𝑛 ) ⊊ 𝑧 ) )
35 pssdifcom1 ( ( 𝑧𝐴𝑛𝐴 ) → ( ( 𝐴𝑧 ) ⊊ 𝑛 ↔ ( 𝐴𝑛 ) ⊊ 𝑧 ) )
36 33 34 35 fin23lem11 ( 𝑏 ⊆ 𝒫 𝐴 → ( ∃ 𝑧 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ∀ 𝑤 ∈ { 𝑐 ∈ 𝒫 𝐴 ∣ ( 𝐴𝑐 ) ∈ 𝑏 } ¬ 𝑤𝑧 → ∃ 𝑚𝑏𝑛𝑏 ¬ 𝑚𝑛 ) )
37 7 32 36 sylc ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → ∃ 𝑚𝑏𝑛𝑏 ¬ 𝑚𝑛 )
38 simp3r ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → [] Or 𝑏 )
39 sorpssuni ( [] Or 𝑏 → ( ∃ 𝑚𝑏𝑛𝑏 ¬ 𝑚𝑛 𝑏𝑏 ) )
40 38 39 syl ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → ( ∃ 𝑚𝑏𝑛𝑏 ¬ 𝑚𝑛 𝑏𝑏 ) )
41 37 40 mpbid ( ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ∧ ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) ) → 𝑏𝑏 )
42 41 3exp ( ( 𝐴𝑉𝑏 ⊆ 𝒫 𝐴 ) → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) → ( ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) → 𝑏𝑏 ) ) )
43 6 42 sylan2 ( ( 𝐴𝑉𝑏 ∈ 𝒫 𝒫 𝐴 ) → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) → ( ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) → 𝑏𝑏 ) ) )
44 43 ralrimdva ( 𝐴𝑉 → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) → ∀ 𝑏 ∈ 𝒫 𝒫 𝐴 ( ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) → 𝑏𝑏 ) ) )
45 isfin2 ( 𝐴𝑉 → ( 𝐴 ∈ FinII ↔ ∀ 𝑏 ∈ 𝒫 𝒫 𝐴 ( ( 𝑏 ≠ ∅ ∧ [] Or 𝑏 ) → 𝑏𝑏 ) ) )
46 44 45 sylibrd ( 𝐴𝑉 → ( ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) → 𝐴 ∈ FinII ) )
47 5 46 impbid2 ( 𝐴𝑉 → ( 𝐴 ∈ FinII ↔ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [] Or 𝑦 ) → 𝑦𝑦 ) ) )