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