pwsdompw

Description: Lemma for domtriom . This is the equinumerosity version of the algebraic identity sum_ k e. n ( 2 ^ k ) = ( 2 ^ n ) - 1 . (Contributed by Mario Carneiro, 7-Feb-2013)

		Ref	Expression
	Assertion	pwsdompw	$⊢ (n \in ω \land \forall k \in suc n B (k) \approx 𝒫 k) \to ⋃_{k \in n} B (k) ≺ B (n)$

Proof

Step	Hyp	Ref	Expression
1		suceq	$⊢ n = \emptyset \to suc n = suc \emptyset$
2	1	raleqdv	$⊢ n = \emptyset \to (\forall k \in suc n B (k) \approx 𝒫 k \leftrightarrow \forall k \in suc \emptyset B (k) \approx 𝒫 k)$
3		iuneq1	$⊢ n = \emptyset \to ⋃_{k \in n} B (k) = ⋃_{k \in \emptyset} B (k)$
4		fveq2	$⊢ n = \emptyset \to B (n) = B (\emptyset)$
5	3 4	breq12d	$⊢ n = \emptyset \to (⋃_{k \in n} B (k) ≺ B (n) \leftrightarrow ⋃_{k \in \emptyset} B (k) ≺ B (\emptyset))$
6	2 5	imbi12d	$⊢ n = \emptyset \to ((\forall k \in suc n B (k) \approx 𝒫 k \to ⋃_{k \in n} B (k) ≺ B (n)) \leftrightarrow (\forall k \in suc \emptyset B (k) \approx 𝒫 k \to ⋃_{k \in \emptyset} B (k) ≺ B (\emptyset)))$
7		suceq	$⊢ n = m \to suc n = suc m$
8	7	raleqdv	$⊢ n = m \to (\forall k \in suc n B (k) \approx 𝒫 k \leftrightarrow \forall k \in suc m B (k) \approx 𝒫 k)$
9		iuneq1	$⊢ n = m \to ⋃_{k \in n} B (k) = ⋃_{k \in m} B (k)$
10		fveq2	$⊢ n = m \to B (n) = B (m)$
11	9 10	breq12d	$⊢ n = m \to (⋃_{k \in n} B (k) ≺ B (n) \leftrightarrow ⋃_{k \in m} B (k) ≺ B (m))$
12	8 11	imbi12d	$⊢ n = m \to ((\forall k \in suc n B (k) \approx 𝒫 k \to ⋃_{k \in n} B (k) ≺ B (n)) \leftrightarrow (\forall k \in suc m B (k) \approx 𝒫 k \to ⋃_{k \in m} B (k) ≺ B (m)))$
13		suceq	$⊢ n = suc m \to suc n = suc suc m$
14	13	raleqdv	$⊢ n = suc m \to (\forall k \in suc n B (k) \approx 𝒫 k \leftrightarrow \forall k \in suc suc m B (k) \approx 𝒫 k)$
15		iuneq1	$⊢ n = suc m \to ⋃_{k \in n} B (k) = ⋃_{k \in suc m} B (k)$
16		fveq2	$⊢ n = suc m \to B (n) = B (suc m)$
17	15 16	breq12d	$⊢ n = suc m \to (⋃_{k \in n} B (k) ≺ B (n) \leftrightarrow ⋃_{k \in suc m} B (k) ≺ B (suc m))$
18	14 17	imbi12d	$⊢ n = suc m \to ((\forall k \in suc n B (k) \approx 𝒫 k \to ⋃_{k \in n} B (k) ≺ B (n)) \leftrightarrow (\forall k \in suc suc m B (k) \approx 𝒫 k \to ⋃_{k \in suc m} B (k) ≺ B (suc m)))$
19		0iun	$⊢ ⋃_{k \in \emptyset} B (k) = \emptyset$
20		0ex	$⊢ \emptyset \in V$
21	20	sucid	$⊢ \emptyset \in suc \emptyset$
22		fveq2	$⊢ k = \emptyset \to B (k) = B (\emptyset)$
23		pweq	$⊢ k = \emptyset \to 𝒫 k = 𝒫 \emptyset$
24	22 23	breq12d	$⊢ k = \emptyset \to (B (k) \approx 𝒫 k \leftrightarrow B (\emptyset) \approx 𝒫 \emptyset)$
25	24	rspcv	$⊢ \emptyset \in suc \emptyset \to (\forall k \in suc \emptyset B (k) \approx 𝒫 k \to B (\emptyset) \approx 𝒫 \emptyset)$
26	21 25	ax-mp	$⊢ \forall k \in suc \emptyset B (k) \approx 𝒫 k \to B (\emptyset) \approx 𝒫 \emptyset$
27	20	canth2	$⊢ \emptyset ≺ 𝒫 \emptyset$
28		ensym	$⊢ B (\emptyset) \approx 𝒫 \emptyset \to 𝒫 \emptyset \approx B (\emptyset)$
29		sdomentr	$⊢ (\emptyset ≺ 𝒫 \emptyset \land 𝒫 \emptyset \approx B (\emptyset)) \to \emptyset ≺ B (\emptyset)$
30	27 28 29	sylancr	$⊢ B (\emptyset) \approx 𝒫 \emptyset \to \emptyset ≺ B (\emptyset)$
31	26 30	syl	$⊢ \forall k \in suc \emptyset B (k) \approx 𝒫 k \to \emptyset ≺ B (\emptyset)$
32	19 31	eqbrtrid	$⊢ \forall k \in suc \emptyset B (k) \approx 𝒫 k \to ⋃_{k \in \emptyset} B (k) ≺ B (\emptyset)$
33		sssucid	$⊢ suc m \subseteq suc suc m$
34		ssralv	$⊢ suc m \subseteq suc suc m \to (\forall k \in suc suc m B (k) \approx 𝒫 k \to \forall k \in suc m B (k) \approx 𝒫 k)$
35	33 34	ax-mp	$⊢ \forall k \in suc suc m B (k) \approx 𝒫 k \to \forall k \in suc m B (k) \approx 𝒫 k$
36		pm2.27	$⊢ \forall k \in suc m B (k) \approx 𝒫 k \to ((\forall k \in suc m B (k) \approx 𝒫 k \to ⋃_{k \in m} B (k) ≺ B (m)) \to ⋃_{k \in m} B (k) ≺ B (m))$
37	35 36	syl	$⊢ \forall k \in suc suc m B (k) \approx 𝒫 k \to ((\forall k \in suc m B (k) \approx 𝒫 k \to ⋃_{k \in m} B (k) ≺ B (m)) \to ⋃_{k \in m} B (k) ≺ B (m))$
38	37	adantl	$⊢ (m \in ω \land \forall k \in suc suc m B (k) \approx 𝒫 k) \to ((\forall k \in suc m B (k) \approx 𝒫 k \to ⋃_{k \in m} B (k) ≺ B (m)) \to ⋃_{k \in m} B (k) ≺ B (m))$
39		vex	$⊢ m \in V$
40	39	sucid	$⊢ m \in suc m$
41		elelsuc	$⊢ m \in suc m \to m \in suc suc m$
42		fveq2	$⊢ k = m \to B (k) = B (m)$
43		pweq	$⊢ k = m \to 𝒫 k = 𝒫 m$
44	42 43	breq12d	$⊢ k = m \to (B (k) \approx 𝒫 k \leftrightarrow B (m) \approx 𝒫 m)$
45	44	rspcv	$⊢ m \in suc suc m \to (\forall k \in suc suc m B (k) \approx 𝒫 k \to B (m) \approx 𝒫 m)$
46	40 41 45	mp2b	$⊢ \forall k \in suc suc m B (k) \approx 𝒫 k \to B (m) \approx 𝒫 m$
47		djuen	$⊢ (B (m) \approx 𝒫 m \land B (m) \approx 𝒫 m) \to (B (m) ⊔︀ B (m)) \approx (𝒫 m ⊔︀ 𝒫 m)$
48	46 46 47	syl2anc	$⊢ \forall k \in suc suc m B (k) \approx 𝒫 k \to (B (m) ⊔︀ B (m)) \approx (𝒫 m ⊔︀ 𝒫 m)$
49		pwdju1	$⊢ m \in ω \to (𝒫 m ⊔︀ 𝒫 m) \approx 𝒫 (m ⊔︀ 1_{𝑜})$
50		nnord	$⊢ m \in ω \to Ord m$
51		ordirr	$⊢ Ord m \to \neg m \in m$
52	50 51	syl	$⊢ m \in ω \to \neg m \in m$
53		dju1en	$⊢ (m \in ω \land \neg m \in m) \to (m ⊔︀ 1_{𝑜}) \approx suc m$
54	52 53	mpdan	$⊢ m \in ω \to (m ⊔︀ 1_{𝑜}) \approx suc m$
55		pwen	$⊢ (m ⊔︀ 1_{𝑜}) \approx suc m \to 𝒫 (m ⊔︀ 1_{𝑜}) \approx 𝒫 suc m$
56	54 55	syl	$⊢ m \in ω \to 𝒫 (m ⊔︀ 1_{𝑜}) \approx 𝒫 suc m$
57		entr	$⊢ ((𝒫 m ⊔︀ 𝒫 m) \approx 𝒫 (m ⊔︀ 1_{𝑜}) \land 𝒫 (m ⊔︀ 1_{𝑜}) \approx 𝒫 suc m) \to (𝒫 m ⊔︀ 𝒫 m) \approx 𝒫 suc m$
58	49 56 57	syl2anc	$⊢ m \in ω \to (𝒫 m ⊔︀ 𝒫 m) \approx 𝒫 suc m$
59		entr	$⊢ ((B (m) ⊔︀ B (m)) \approx (𝒫 m ⊔︀ 𝒫 m) \land (𝒫 m ⊔︀ 𝒫 m) \approx 𝒫 suc m) \to (B (m) ⊔︀ B (m)) \approx 𝒫 suc m$
60	48 58 59	syl2an	$⊢ (\forall k \in suc suc m B (k) \approx 𝒫 k \land m \in ω) \to (B (m) ⊔︀ B (m)) \approx 𝒫 suc m$
61	39	sucex	$⊢ suc m \in V$
62	61	sucid	$⊢ suc m \in suc suc m$
63		fveq2	$⊢ k = suc m \to B (k) = B (suc m)$
64		pweq	$⊢ k = suc m \to 𝒫 k = 𝒫 suc m$
65	63 64	breq12d	$⊢ k = suc m \to (B (k) \approx 𝒫 k \leftrightarrow B (suc m) \approx 𝒫 suc m)$
66	65	rspcv	$⊢ suc m \in suc suc m \to (\forall k \in suc suc m B (k) \approx 𝒫 k \to B (suc m) \approx 𝒫 suc m)$
67	62 66	ax-mp	$⊢ \forall k \in suc suc m B (k) \approx 𝒫 k \to B (suc m) \approx 𝒫 suc m$
68	67	ensymd	$⊢ \forall k \in suc suc m B (k) \approx 𝒫 k \to 𝒫 suc m \approx B (suc m)$
69	68	adantr	$⊢ (\forall k \in suc suc m B (k) \approx 𝒫 k \land m \in ω) \to 𝒫 suc m \approx B (suc m)$
70		entr	$⊢ ((B (m) ⊔︀ B (m)) \approx 𝒫 suc m \land 𝒫 suc m \approx B (suc m)) \to (B (m) ⊔︀ B (m)) \approx B (suc m)$
71	60 69 70	syl2anc	$⊢ (\forall k \in suc suc m B (k) \approx 𝒫 k \land m \in ω) \to (B (m) ⊔︀ B (m)) \approx B (suc m)$
72	71	ancoms	$⊢ (m \in ω \land \forall k \in suc suc m B (k) \approx 𝒫 k) \to (B (m) ⊔︀ B (m)) \approx B (suc m)$
73		nnfi	$⊢ m \in ω \to m \in Fin$
74		pwfi	$⊢ m \in Fin \leftrightarrow 𝒫 m \in Fin$
75		isfinite	$⊢ 𝒫 m \in Fin \leftrightarrow 𝒫 m ≺ ω$
76	74 75	bitri	$⊢ m \in Fin \leftrightarrow 𝒫 m ≺ ω$
77	73 76	sylib	$⊢ m \in ω \to 𝒫 m ≺ ω$
78		ensdomtr	$⊢ (B (m) \approx 𝒫 m \land 𝒫 m ≺ ω) \to B (m) ≺ ω$
79	46 77 78	syl2an	$⊢ (\forall k \in suc suc m B (k) \approx 𝒫 k \land m \in ω) \to B (m) ≺ ω$
80		isfinite	$⊢ B (m) \in Fin \leftrightarrow B (m) ≺ ω$
81	79 80	sylibr	$⊢ (\forall k \in suc suc m B (k) \approx 𝒫 k \land m \in ω) \to B (m) \in Fin$
82	81	ancoms	$⊢ (m \in ω \land \forall k \in suc suc m B (k) \approx 𝒫 k) \to B (m) \in Fin$
83	39 42	iunsuc	$⊢ ⋃_{k \in suc m} B (k) = ⋃_{k \in m} B (k) \cup B (m)$
84		fvex	$⊢ B (k) \in V$
85	39 84	iunex	$⊢ ⋃_{k \in m} B (k) \in V$
86		fvex	$⊢ B (m) \in V$
87		undjudom	$⊢ (⋃_{k \in m} B (k) \in V \land B (m) \in V) \to (⋃_{k \in m} B (k) \cup B (m)) ≼ (⋃_{k \in m} B (k) ⊔︀ B (m))$
88	85 86 87	mp2an	$⊢ (⋃_{k \in m} B (k) \cup B (m)) ≼ (⋃_{k \in m} B (k) ⊔︀ B (m))$
89	83 88	eqbrtri	$⊢ ⋃_{k \in suc m} B (k) ≼ (⋃_{k \in m} B (k) ⊔︀ B (m))$
90		sdomtr	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) ≺ ω) \to ⋃_{k \in m} B (k) ≺ ω$
91	80 90	sylan2b	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to ⋃_{k \in m} B (k) ≺ ω$
92		isfinite	$⊢ ⋃_{k \in m} B (k) \in Fin \leftrightarrow ⋃_{k \in m} B (k) ≺ ω$
93	91 92	sylibr	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to ⋃_{k \in m} B (k) \in Fin$
94		finnum	$⊢ ⋃_{k \in m} B (k) \in Fin \to ⋃_{k \in m} B (k) \in dom card$
95	93 94	syl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to ⋃_{k \in m} B (k) \in dom card$
96		finnum	$⊢ B (m) \in Fin \to B (m) \in dom card$
97	96	adantl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to B (m) \in dom card$
98		cardadju	$⊢ (⋃_{k \in m} B (k) \in dom card \land B (m) \in dom card) \to (⋃_{k \in m} B (k) ⊔︀ B (m)) \approx (card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m)))$
99	95 97 98	syl2anc	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to (⋃_{k \in m} B (k) ⊔︀ B (m)) \approx (card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m)))$
100		ficardom	$⊢ ⋃_{k \in m} B (k) \in Fin \to card (⋃_{k \in m} B (k)) \in ω$
101	93 100	syl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to card (⋃_{k \in m} B (k)) \in ω$
102		ficardom	$⊢ B (m) \in Fin \to card (B (m)) \in ω$
103	102	adantl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to card (B (m)) \in ω$
104		cardid2	$⊢ ⋃_{k \in m} B (k) \in dom card \to card (⋃_{k \in m} B (k)) \approx ⋃_{k \in m} B (k)$
105	93 94 104	3syl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to card (⋃_{k \in m} B (k)) \approx ⋃_{k \in m} B (k)$
106		simpl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to ⋃_{k \in m} B (k) ≺ B (m)$
107		cardid2	$⊢ B (m) \in dom card \to card (B (m)) \approx B (m)$
108		ensym	$⊢ card (B (m)) \approx B (m) \to B (m) \approx card (B (m))$
109	96 107 108	3syl	$⊢ B (m) \in Fin \to B (m) \approx card (B (m))$
110	109	adantl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to B (m) \approx card (B (m))$
111		ensdomtr	$⊢ (card (⋃_{k \in m} B (k)) \approx ⋃_{k \in m} B (k) \land ⋃_{k \in m} B (k) ≺ B (m)) \to card (⋃_{k \in m} B (k)) ≺ B (m)$
112		sdomentr	$⊢ (card (⋃_{k \in m} B (k)) ≺ B (m) \land B (m) \approx card (B (m))) \to card (⋃_{k \in m} B (k)) ≺ card (B (m))$
113	111 112	sylan	$⊢ ((card (⋃_{k \in m} B (k)) \approx ⋃_{k \in m} B (k) \land ⋃_{k \in m} B (k) ≺ B (m)) \land B (m) \approx card (B (m))) \to card (⋃_{k \in m} B (k)) ≺ card (B (m))$
114	105 106 110 113	syl21anc	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to card (⋃_{k \in m} B (k)) ≺ card (B (m))$
115		cardon	$⊢ card (⋃_{k \in m} B (k)) \in On$
116		cardon	$⊢ card (B (m)) \in On$
117		onenon	$⊢ card (B (m)) \in On \to card (B (m)) \in dom card$
118	116 117	ax-mp	$⊢ card (B (m)) \in dom card$
119		cardsdomel	$⊢ (card (⋃_{k \in m} B (k)) \in On \land card (B (m)) \in dom card) \to (card (⋃_{k \in m} B (k)) ≺ card (B (m)) \leftrightarrow card (⋃_{k \in m} B (k)) \in card (card (B (m))))$
120	115 118 119	mp2an	$⊢ card (⋃_{k \in m} B (k)) ≺ card (B (m)) \leftrightarrow card (⋃_{k \in m} B (k)) \in card (card (B (m)))$
121		cardidm	$⊢ card (card (B (m))) = card (B (m))$
122	121	eleq2i	$⊢ card (⋃_{k \in m} B (k)) \in card (card (B (m))) \leftrightarrow card (⋃_{k \in m} B (k)) \in card (B (m))$
123	120 122	bitri	$⊢ card (⋃_{k \in m} B (k)) ≺ card (B (m)) \leftrightarrow card (⋃_{k \in m} B (k)) \in card (B (m))$
124	114 123	sylib	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to card (⋃_{k \in m} B (k)) \in card (B (m))$
125		nnaordr	$⊢ (card (⋃_{k \in m} B (k)) \in ω \land card (B (m)) \in ω \land card (B (m)) \in ω) \to (card (⋃_{k \in m} B (k)) \in card (B (m)) \leftrightarrow card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m)) \in (card (B (m)) +_{𝑜} card (B (m))))$
126	125	biimpa	$⊢ ((card (⋃_{k \in m} B (k)) \in ω \land card (B (m)) \in ω \land card (B (m)) \in ω) \land card (⋃_{k \in m} B (k)) \in card (B (m))) \to card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m)) \in (card (B (m)) +_{𝑜} card (B (m)))$
127	101 103 103 124 126	syl31anc	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m)) \in (card (B (m)) +_{𝑜} card (B (m)))$
128		nnacl	$⊢ (card (B (m)) \in ω \land card (B (m)) \in ω) \to card (B (m)) +_{𝑜} card (B (m)) \in ω$
129	102 102 128	syl2anc	$⊢ B (m) \in Fin \to card (B (m)) +_{𝑜} card (B (m)) \in ω$
130		cardnn	$⊢ card (B (m)) +_{𝑜} card (B (m)) \in ω \to card (card (B (m)) +_{𝑜} card (B (m))) = card (B (m)) +_{𝑜} card (B (m))$
131	129 130	syl	$⊢ B (m) \in Fin \to card (card (B (m)) +_{𝑜} card (B (m))) = card (B (m)) +_{𝑜} card (B (m))$
132	131	adantl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to card (card (B (m)) +_{𝑜} card (B (m))) = card (B (m)) +_{𝑜} card (B (m))$
133	127 132	eleqtrrd	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m)) \in card (card (B (m)) +_{𝑜} card (B (m)))$
134		cardsdomelir	$⊢ card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m)) \in card (card (B (m)) +_{𝑜} card (B (m))) \to (card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m))) ≺ (card (B (m)) +_{𝑜} card (B (m)))$
135	133 134	syl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to (card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m))) ≺ (card (B (m)) +_{𝑜} card (B (m)))$
136		ensdomtr	$⊢ ((⋃_{k \in m} B (k) ⊔︀ B (m)) \approx (card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m))) \land (card (⋃_{k \in m} B (k)) +_{𝑜} card (B (m))) ≺ (card (B (m)) +_{𝑜} card (B (m)))) \to (⋃_{k \in m} B (k) ⊔︀ B (m)) ≺ (card (B (m)) +_{𝑜} card (B (m)))$
137	99 135 136	syl2anc	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to (⋃_{k \in m} B (k) ⊔︀ B (m)) ≺ (card (B (m)) +_{𝑜} card (B (m)))$
138		cardadju	$⊢ (B (m) \in dom card \land B (m) \in dom card) \to (B (m) ⊔︀ B (m)) \approx (card (B (m)) +_{𝑜} card (B (m)))$
139	96 96 138	syl2anc	$⊢ B (m) \in Fin \to (B (m) ⊔︀ B (m)) \approx (card (B (m)) +_{𝑜} card (B (m)))$
140	139	ensymd	$⊢ B (m) \in Fin \to (card (B (m)) +_{𝑜} card (B (m))) \approx (B (m) ⊔︀ B (m))$
141	140	adantl	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to (card (B (m)) +_{𝑜} card (B (m))) \approx (B (m) ⊔︀ B (m))$
142		sdomentr	$⊢ ((⋃_{k \in m} B (k) ⊔︀ B (m)) ≺ (card (B (m)) +_{𝑜} card (B (m))) \land (card (B (m)) +_{𝑜} card (B (m))) \approx (B (m) ⊔︀ B (m))) \to (⋃_{k \in m} B (k) ⊔︀ B (m)) ≺ (B (m) ⊔︀ B (m))$
143	137 141 142	syl2anc	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to (⋃_{k \in m} B (k) ⊔︀ B (m)) ≺ (B (m) ⊔︀ B (m))$
144		domsdomtr	$⊢ (⋃_{k \in suc m} B (k) ≼ (⋃_{k \in m} B (k) ⊔︀ B (m)) \land (⋃_{k \in m} B (k) ⊔︀ B (m)) ≺ (B (m) ⊔︀ B (m))) \to ⋃_{k \in suc m} B (k) ≺ (B (m) ⊔︀ B (m))$
145	89 143 144	sylancr	$⊢ (⋃_{k \in m} B (k) ≺ B (m) \land B (m) \in Fin) \to ⋃_{k \in suc m} B (k) ≺ (B (m) ⊔︀ B (m))$
146	145	expcom	$⊢ B (m) \in Fin \to (⋃_{k \in m} B (k) ≺ B (m) \to ⋃_{k \in suc m} B (k) ≺ (B (m) ⊔︀ B (m)))$
147	82 146	syl	$⊢ (m \in ω \land \forall k \in suc suc m B (k) \approx 𝒫 k) \to (⋃_{k \in m} B (k) ≺ B (m) \to ⋃_{k \in suc m} B (k) ≺ (B (m) ⊔︀ B (m)))$
148		sdomentr	$⊢ (⋃_{k \in suc m} B (k) ≺ (B (m) ⊔︀ B (m)) \land (B (m) ⊔︀ B (m)) \approx B (suc m)) \to ⋃_{k \in suc m} B (k) ≺ B (suc m)$
149	148	expcom	$⊢ (B (m) ⊔︀ B (m)) \approx B (suc m) \to (⋃_{k \in suc m} B (k) ≺ (B (m) ⊔︀ B (m)) \to ⋃_{k \in suc m} B (k) ≺ B (suc m))$
150	72 147 149	sylsyld	$⊢ (m \in ω \land \forall k \in suc suc m B (k) \approx 𝒫 k) \to (⋃_{k \in m} B (k) ≺ B (m) \to ⋃_{k \in suc m} B (k) ≺ B (suc m))$
151	38 150	syld	$⊢ (m \in ω \land \forall k \in suc suc m B (k) \approx 𝒫 k) \to ((\forall k \in suc m B (k) \approx 𝒫 k \to ⋃_{k \in m} B (k) ≺ B (m)) \to ⋃_{k \in suc m} B (k) ≺ B (suc m))$
152	151	ex	$⊢ m \in ω \to (\forall k \in suc suc m B (k) \approx 𝒫 k \to ((\forall k \in suc m B (k) \approx 𝒫 k \to ⋃_{k \in m} B (k) ≺ B (m)) \to ⋃_{k \in suc m} B (k) ≺ B (suc m)))$
153	152	com23	$⊢ m \in ω \to ((\forall k \in suc m B (k) \approx 𝒫 k \to ⋃_{k \in m} B (k) ≺ B (m)) \to (\forall k \in suc suc m B (k) \approx 𝒫 k \to ⋃_{k \in suc m} B (k) ≺ B (suc m)))$
154	6 12 18 32 153	finds1	$⊢ n \in ω \to (\forall k \in suc n B (k) \approx 𝒫 k \to ⋃_{k \in n} B (k) ≺ B (n))$
155	154	imp	$⊢ (n \in ω \land \forall k \in suc n B (k) \approx 𝒫 k) \to ⋃_{k \in n} B (k) ≺ B (n)$

Metamath Proof Explorer

Theorem pwsdompw

Proof