# Metamath Proof Explorer

## Theorem fin2i

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

Ref Expression
Assertion fin2i ${⊢}\left(\left({A}\in {\mathrm{Fin}}^{II}\wedge {B}\subseteq 𝒫{A}\right)\wedge \left({B}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{B}\right)\right)\to \bigcup {B}\in {B}$

### Proof

Step Hyp Ref Expression
1 neeq1 ${⊢}{y}={B}\to \left({y}\ne \varnothing ↔{B}\ne \varnothing \right)$
2 soeq2 ${⊢}{y}={B}\to \left(\left[\subset \right]\mathrm{Or}{y}↔\left[\subset \right]\mathrm{Or}{B}\right)$
3 1 2 anbi12d ${⊢}{y}={B}\to \left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)↔\left({B}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{B}\right)\right)$
4 unieq ${⊢}{y}={B}\to \bigcup {y}=\bigcup {B}$
5 id ${⊢}{y}={B}\to {y}={B}$
6 4 5 eleq12d ${⊢}{y}={B}\to \left(\bigcup {y}\in {y}↔\bigcup {B}\in {B}\right)$
7 3 6 imbi12d ${⊢}{y}={B}\to \left(\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)↔\left(\left({B}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{B}\right)\to \bigcup {B}\in {B}\right)\right)$
8 isfin2 ${⊢}{A}\in {\mathrm{Fin}}^{II}\to \left({A}\in {\mathrm{Fin}}^{II}↔\forall {y}\in 𝒫𝒫{A}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right)$
9 8 ibi ${⊢}{A}\in {\mathrm{Fin}}^{II}\to \forall {y}\in 𝒫𝒫{A}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)$
10 9 adantr ${⊢}\left({A}\in {\mathrm{Fin}}^{II}\wedge {B}\subseteq 𝒫{A}\right)\to \forall {y}\in 𝒫𝒫{A}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)$
11 pwexg ${⊢}{A}\in {\mathrm{Fin}}^{II}\to 𝒫{A}\in \mathrm{V}$
12 elpw2g ${⊢}𝒫{A}\in \mathrm{V}\to \left({B}\in 𝒫𝒫{A}↔{B}\subseteq 𝒫{A}\right)$
13 11 12 syl ${⊢}{A}\in {\mathrm{Fin}}^{II}\to \left({B}\in 𝒫𝒫{A}↔{B}\subseteq 𝒫{A}\right)$
14 13 biimpar ${⊢}\left({A}\in {\mathrm{Fin}}^{II}\wedge {B}\subseteq 𝒫{A}\right)\to {B}\in 𝒫𝒫{A}$
15 7 10 14 rspcdva ${⊢}\left({A}\in {\mathrm{Fin}}^{II}\wedge {B}\subseteq 𝒫{A}\right)\to \left(\left({B}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{B}\right)\to \bigcup {B}\in {B}\right)$
16 15 imp ${⊢}\left(\left({A}\in {\mathrm{Fin}}^{II}\wedge {B}\subseteq 𝒫{A}\right)\wedge \left({B}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{B}\right)\right)\to \bigcup {B}\in {B}$