enfin2i

Description: II-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015)

		Ref	Expression
	Assertion	enfin2i	$⊢ A \approx B \to (A \in {Fin}^{II} \to B \in {Fin}^{II})$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B$
2		elpwi	$⊢ x \in 𝒫 𝒫 B \to x \subseteq 𝒫 B$
3		imauni	$⊢ f [⋃ \{y \in 𝒫 A \| f [y] \in x\}] = ⋃_{z \in \{y \in 𝒫 A \| f [y] \in x\}} f [z]$
4		vex	$⊢ f \in V$
5	4	imaex	$⊢ f [z] \in V$
6	5	dfiun2	$⊢ ⋃_{z \in \{y \in 𝒫 A \| f [y] \in x\}} f [z] = ⋃ \{w \| \exists z \in \{y \in 𝒫 A \| f [y] \in x\} w = f [z]\}$
7	3 6	eqtri	$⊢ f [⋃ \{y \in 𝒫 A \| f [y] \in x\}] = ⋃ \{w \| \exists z \in \{y \in 𝒫 A \| f [y] \in x\} w = f [z]\}$
8		imaeq2	$⊢ y = z \to f [y] = f [z]$
9	8	eleq1d	$⊢ y = z \to (f [y] \in x \leftrightarrow f [z] \in x)$
10	9	rexrab	$⊢ \exists z \in \{y \in 𝒫 A \| f [y] \in x\} w = f [z] \leftrightarrow \exists z \in 𝒫 A (f [z] \in x \land w = f [z])$
11		eleq1	$⊢ w = f [z] \to (w \in x \leftrightarrow f [z] \in x)$
12	11	biimparc	$⊢ (f [z] \in x \land w = f [z]) \to w \in x$
13	12	rexlimivw	$⊢ \exists z \in 𝒫 A (f [z] \in x \land w = f [z]) \to w \in x$
14		cnvimass	$⊢ f^{-1} [w] \subseteq dom f$
15		f1odm	$⊢ f : A \underset{1-1 onto}{⟶} B \to dom f = A$
16	15	ad3antrrr	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to dom f = A$
17	14 16	sseqtrid	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to f^{-1} [w] \subseteq A$
18	4	cnvex	$⊢ f^{-1} \in V$
19	18	imaex	$⊢ f^{-1} [w] \in V$
20	19	elpw	$⊢ f^{-1} [w] \in 𝒫 A \leftrightarrow f^{-1} [w] \subseteq A$
21	17 20	sylibr	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to f^{-1} [w] \in 𝒫 A$
22		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
23	22	ad3antrrr	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to f : A \underset{onto}{⟶} B$
24		simprl	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to x \subseteq 𝒫 B$
25	24	sselda	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to w \in 𝒫 B$
26	25	elpwid	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to w \subseteq B$
27		foimacnv	$⊢ (f : A \underset{onto}{⟶} B \land w \subseteq B) \to f [f^{-1} [w]] = w$
28	23 26 27	syl2anc	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to f [f^{-1} [w]] = w$
29	28	eqcomd	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to w = f [f^{-1} [w]]$
30		simpr	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to w \in x$
31	29 30	eqeltrrd	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to f [f^{-1} [w]] \in x$
32		imaeq2	$⊢ z = f^{-1} [w] \to f [z] = f [f^{-1} [w]]$
33	32	eleq1d	$⊢ z = f^{-1} [w] \to (f [z] \in x \leftrightarrow f [f^{-1} [w]] \in x)$
34	32	eqeq2d	$⊢ z = f^{-1} [w] \to (w = f [z] \leftrightarrow w = f [f^{-1} [w]])$
35	33 34	anbi12d	$⊢ z = f^{-1} [w] \to ((f [z] \in x \land w = f [z]) \leftrightarrow (f [f^{-1} [w]] \in x \land w = f [f^{-1} [w]]))$
36	35	rspcev	$⊢ (f^{-1} [w] \in 𝒫 A \land (f [f^{-1} [w]] \in x \land w = f [f^{-1} [w]])) \to \exists z \in 𝒫 A (f [z] \in x \land w = f [z])$
37	21 31 29 36	syl12anc	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to \exists z \in 𝒫 A (f [z] \in x \land w = f [z])$
38	37	ex	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to (w \in x \to \exists z \in 𝒫 A (f [z] \in x \land w = f [z]))$
39	13 38	impbid2	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to (\exists z \in 𝒫 A (f [z] \in x \land w = f [z]) \leftrightarrow w \in x)$
40	10 39	syl5bb	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to (\exists z \in \{y \in 𝒫 A \| f [y] \in x\} w = f [z] \leftrightarrow w \in x)$
41	40	abbi1dv	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to \{w \| \exists z \in \{y \in 𝒫 A \| f [y] \in x\} w = f [z]\} = x$
42	41	unieqd	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to ⋃ \{w \| \exists z \in \{y \in 𝒫 A \| f [y] \in x\} w = f [z]\} = ⋃ x$
43	7 42	eqtrid	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to f [⋃ \{y \in 𝒫 A \| f [y] \in x\}] = ⋃ x$
44		simplr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to A \in {Fin}^{II}$
45		ssrab2	$⊢ \{y \in 𝒫 A \| f [y] \in x\} \subseteq 𝒫 A$
46	45	a1i	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to \{y \in 𝒫 A \| f [y] \in x\} \subseteq 𝒫 A$
47		simprrl	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to x \neq \emptyset$
48		n0	$⊢ x \neq \emptyset \leftrightarrow \exists w w \in x$
49	47 48	sylib	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to \exists w w \in x$
50		imaeq2	$⊢ y = f^{-1} [w] \to f [y] = f [f^{-1} [w]]$
51	50	eleq1d	$⊢ y = f^{-1} [w] \to (f [y] \in x \leftrightarrow f [f^{-1} [w]] \in x)$
52	51	rspcev	$⊢ (f^{-1} [w] \in 𝒫 A \land f [f^{-1} [w]] \in x) \to \exists y \in 𝒫 A f [y] \in x$
53	21 31 52	syl2anc	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land w \in x) \to \exists y \in 𝒫 A f [y] \in x$
54	49 53	exlimddv	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to \exists y \in 𝒫 A f [y] \in x$
55		rabn0	$⊢ \{y \in 𝒫 A \| f [y] \in x\} \neq \emptyset \leftrightarrow \exists y \in 𝒫 A f [y] \in x$
56	54 55	sylibr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to \{y \in 𝒫 A \| f [y] \in x\} \neq \emptyset$
57	9	elrab	$⊢ z \in \{y \in 𝒫 A \| f [y] \in x\} \leftrightarrow (z \in 𝒫 A \land f [z] \in x)$
58		imaeq2	$⊢ y = w \to f [y] = f [w]$
59	58	eleq1d	$⊢ y = w \to (f [y] \in x \leftrightarrow f [w] \in x)$
60	59	elrab	$⊢ w \in \{y \in 𝒫 A \| f [y] \in x\} \leftrightarrow (w \in 𝒫 A \land f [w] \in x)$
61	57 60	anbi12i	$⊢ (z \in \{y \in 𝒫 A \| f [y] \in x\} \land w \in \{y \in 𝒫 A \| f [y] \in x\}) \leftrightarrow ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))$
62		simprrr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to [\subset] Or x$
63	62	adantr	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to [\subset] Or x$
64		simprlr	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to f [z] \in x$
65		simprrr	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to f [w] \in x$
66		sorpssi	$⊢ ([\subset] Or x \land (f [z] \in x \land f [w] \in x)) \to (f [z] \subseteq f [w] \lor f [w] \subseteq f [z])$
67	63 64 65 66	syl12anc	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to (f [z] \subseteq f [w] \lor f [w] \subseteq f [z])$
68		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{1-1}{⟶} B$
69	68	ad3antrrr	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to f : A \underset{1-1}{⟶} B$
70		simprll	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to z \in 𝒫 A$
71	70	elpwid	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to z \subseteq A$
72		simprrl	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to w \in 𝒫 A$
73	72	elpwid	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to w \subseteq A$
74		f1imass	$⊢ (f : A \underset{1-1}{⟶} B \land (z \subseteq A \land w \subseteq A)) \to (f [z] \subseteq f [w] \leftrightarrow z \subseteq w)$
75	69 71 73 74	syl12anc	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to (f [z] \subseteq f [w] \leftrightarrow z \subseteq w)$
76		f1imass	$⊢ (f : A \underset{1-1}{⟶} B \land (w \subseteq A \land z \subseteq A)) \to (f [w] \subseteq f [z] \leftrightarrow w \subseteq z)$
77	69 73 71 76	syl12anc	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to (f [w] \subseteq f [z] \leftrightarrow w \subseteq z)$
78	75 77	orbi12d	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to ((f [z] \subseteq f [w] \lor f [w] \subseteq f [z]) \leftrightarrow (z \subseteq w \lor w \subseteq z))$
79	67 78	mpbid	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land ((z \in 𝒫 A \land f [z] \in x) \land (w \in 𝒫 A \land f [w] \in x))) \to (z \subseteq w \lor w \subseteq z)$
80	61 79	sylan2b	$⊢ (((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \land (z \in \{y \in 𝒫 A \| f [y] \in x\} \land w \in \{y \in 𝒫 A \| f [y] \in x\})) \to (z \subseteq w \lor w \subseteq z)$
81	80	ralrimivva	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to \forall z \in \{y \in 𝒫 A \| f [y] \in x\} \forall w \in \{y \in 𝒫 A \| f [y] \in x\} (z \subseteq w \lor w \subseteq z)$
82		sorpss	$⊢ [\subset] Or \{y \in 𝒫 A \| f [y] \in x\} \leftrightarrow \forall z \in \{y \in 𝒫 A \| f [y] \in x\} \forall w \in \{y \in 𝒫 A \| f [y] \in x\} (z \subseteq w \lor w \subseteq z)$
83	81 82	sylibr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to [\subset] Or \{y \in 𝒫 A \| f [y] \in x\}$
84		fin2i	$⊢ ((A \in {Fin}^{II} \land \{y \in 𝒫 A \| f [y] \in x\} \subseteq 𝒫 A) \land (\{y \in 𝒫 A \| f [y] \in x\} \neq \emptyset \land [\subset] Or \{y \in 𝒫 A \| f [y] \in x\})) \to ⋃ \{y \in 𝒫 A \| f [y] \in x\} \in \{y \in 𝒫 A \| f [y] \in x\}$
85	44 46 56 83 84	syl22anc	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to ⋃ \{y \in 𝒫 A \| f [y] \in x\} \in \{y \in 𝒫 A \| f [y] \in x\}$
86		imaeq2	$⊢ z = ⋃ \{y \in 𝒫 A \| f [y] \in x\} \to f [z] = f [⋃ \{y \in 𝒫 A \| f [y] \in x\}]$
87	86	eleq1d	$⊢ z = ⋃ \{y \in 𝒫 A \| f [y] \in x\} \to (f [z] \in x \leftrightarrow f [⋃ \{y \in 𝒫 A \| f [y] \in x\}] \in x)$
88	9	cbvrabv	$⊢ \{y \in 𝒫 A \| f [y] \in x\} = \{z \in 𝒫 A \| f [z] \in x\}$
89	87 88	elrab2	$⊢ ⋃ \{y \in 𝒫 A \| f [y] \in x\} \in \{y \in 𝒫 A \| f [y] \in x\} \leftrightarrow (⋃ \{y \in 𝒫 A \| f [y] \in x\} \in 𝒫 A \land f [⋃ \{y \in 𝒫 A \| f [y] \in x\}] \in x)$
90	89	simprbi	$⊢ ⋃ \{y \in 𝒫 A \| f [y] \in x\} \in \{y \in 𝒫 A \| f [y] \in x\} \to f [⋃ \{y \in 𝒫 A \| f [y] \in x\}] \in x$
91	85 90	syl	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to f [⋃ \{y \in 𝒫 A \| f [y] \in x\}] \in x$
92	43 91	eqeltrrd	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land (x \subseteq 𝒫 B \land (x \neq \emptyset \land [\subset] Or x))) \to ⋃ x \in x$
93	92	expr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land x \subseteq 𝒫 B) \to ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x)$
94	2 93	sylan2	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \land x \in 𝒫 𝒫 B) \to ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x)$
95	94	ralrimiva	$⊢ (f : A \underset{1-1 onto}{⟶} B \land A \in {Fin}^{II}) \to \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x)$
96	95	ex	$⊢ f : A \underset{1-1 onto}{⟶} B \to (A \in {Fin}^{II} \to \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x))$
97	96	exlimiv	$⊢ \exists f f : A \underset{1-1 onto}{⟶} B \to (A \in {Fin}^{II} \to \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x))$
98	1 97	sylbi	$⊢ A \approx B \to (A \in {Fin}^{II} \to \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x))$
99		relen	$⊢ Rel \approx$
100	99	brrelex2i	$⊢ A \approx B \to B \in V$
101		isfin2	$⊢ B \in V \to (B \in {Fin}^{II} \leftrightarrow \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x))$
102	100 101	syl	$⊢ A \approx B \to (B \in {Fin}^{II} \leftrightarrow \forall x \in 𝒫 𝒫 B ((x \neq \emptyset \land [\subset] Or x) \to ⋃ x \in x))$
103	98 102	sylibrd	$⊢ A \approx B \to (A \in {Fin}^{II} \to B \in {Fin}^{II})$

Metamath Proof Explorer

Theorem enfin2i

Proof