This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑦 ) → ∩ 𝑦 ∈ 𝑦 ) ) )