Theorem fin2i

Description: Property of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	fin2i	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ∪ 𝐵 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		neeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
2		soeq2	⊢ ( 𝑦 = 𝐵 → ( [⊊] Or 𝑦 ↔ [⊊] Or 𝐵 ) )
3	1 2	anbi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) ↔ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) )
4		unieq	⊢ ( 𝑦 = 𝐵 → ∪ 𝑦 = ∪ 𝐵 )
5		id	⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
6	4 5	eleq12d	⊢ ( 𝑦 = 𝐵 → ( ∪ 𝑦 ∈ 𝑦 ↔ ∪ 𝐵 ∈ 𝐵 ) )
7	3 6	imbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) ↔ ( ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) → ∪ 𝐵 ∈ 𝐵 ) ) )
8		isfin2	⊢ ( 𝐴 ∈ FinII → ( 𝐴 ∈ FinII ↔ ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) ) )
9	8	ibi	⊢ ( 𝐴 ∈ FinII → ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) )
10	9	adantr	⊢ ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴 ) → ∀ 𝑦 ∈ 𝒫 𝒫 𝐴 ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ 𝑦 ) )
11		pwexg	⊢ ( 𝐴 ∈ FinII → 𝒫 𝐴 ∈ V )
12		elpw2g	⊢ ( 𝒫 𝐴 ∈ V → ( 𝐵 ∈ 𝒫 𝒫 𝐴 ↔ 𝐵 ⊆ 𝒫 𝐴 ) )
13	11 12	syl	⊢ ( 𝐴 ∈ FinII → ( 𝐵 ∈ 𝒫 𝒫 𝐴 ↔ 𝐵 ⊆ 𝒫 𝐴 ) )
14	13	biimpar	⊢ ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴 ) → 𝐵 ∈ 𝒫 𝒫 𝐴 )
15	7 10 14	rspcdva	⊢ ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴 ) → ( ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) → ∪ 𝐵 ∈ 𝐵 ) )
16	15	imp	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ [⊊] Or 𝐵 ) ) → ∪ 𝐵 ∈ 𝐵 )