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

Metamath Proof Explorer

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 𝐵 ) ) → ∪ 𝐵 ∈ 𝐵 )