domtriomlem

	Ref	Expression
Hypotheses	domtriomlem.1	$⊢ A \in V$
	domtriomlem.2	$⊢ B = \{y \| (y \subseteq A \land y \approx 𝒫 n)\}$
	domtriomlem.3	$⊢ C = (n \in ω ⟼ b (n) ∖ ⋃_{k \in n} b (k))$
Assertion	domtriomlem	$⊢ \neg A \in Fin \to ω ≼ A$

Proof

Step	Hyp	Ref	Expression
1		domtriomlem.1	$⊢ A \in V$
2		domtriomlem.2	$⊢ B = \{y \| (y \subseteq A \land y \approx 𝒫 n)\}$
3		domtriomlem.3	$⊢ C = (n \in ω ⟼ b (n) ∖ ⋃_{k \in n} b (k))$
4	1	pwex	$⊢ 𝒫 A \in V$
5		simpl	$⊢ (y \subseteq A \land y \approx 𝒫 n) \to y \subseteq A$
6	5	ss2abi	$⊢ \{y \| (y \subseteq A \land y \approx 𝒫 n)\} \subseteq \{y \| y \subseteq A\}$
7		df-pw	$⊢ 𝒫 A = \{y \| y \subseteq A\}$
8	6 7	sseqtrri	$⊢ \{y \| (y \subseteq A \land y \approx 𝒫 n)\} \subseteq 𝒫 A$
9	4 8	ssexi	$⊢ \{y \| (y \subseteq A \land y \approx 𝒫 n)\} \in V$
10	2 9	eqeltri	$⊢ B \in V$
11		omex	$⊢ ω \in V$
12	11	enref	$⊢ ω \approx ω$
13	10 12	axcc3	$⊢ \exists b (b Fn ω \land \forall n \in ω (B \neq \emptyset \to b (n) \in B))$
14		nfv	$⊢ Ⅎ n \neg A \in Fin$
15		nfra1	$⊢ Ⅎ n \forall n \in ω (B \neq \emptyset \to b (n) \in B)$
16	14 15	nfan	$⊢ Ⅎ n (\neg A \in Fin \land \forall n \in ω (B \neq \emptyset \to b (n) \in B))$
17		nnfi	$⊢ n \in ω \to n \in Fin$
18		pwfi	$⊢ n \in Fin \leftrightarrow 𝒫 n \in Fin$
19	17 18	sylib	$⊢ n \in ω \to 𝒫 n \in Fin$
20		ficardom	$⊢ 𝒫 n \in Fin \to card (𝒫 n) \in ω$
21		isinf	$⊢ \neg A \in Fin \to \forall m \in ω \exists y (y \subseteq A \land y \approx m)$
22		breq2	$⊢ m = card (𝒫 n) \to (y \approx m \leftrightarrow y \approx card (𝒫 n))$
23	22	anbi2d	$⊢ m = card (𝒫 n) \to ((y \subseteq A \land y \approx m) \leftrightarrow (y \subseteq A \land y \approx card (𝒫 n)))$
24	23	exbidv	$⊢ m = card (𝒫 n) \to (\exists y (y \subseteq A \land y \approx m) \leftrightarrow \exists y (y \subseteq A \land y \approx card (𝒫 n)))$
25	24	rspcv	$⊢ card (𝒫 n) \in ω \to (\forall m \in ω \exists y (y \subseteq A \land y \approx m) \to \exists y (y \subseteq A \land y \approx card (𝒫 n)))$
26	21 25	syl5	$⊢ card (𝒫 n) \in ω \to (\neg A \in Fin \to \exists y (y \subseteq A \land y \approx card (𝒫 n)))$
27	19 20 26	3syl	$⊢ n \in ω \to (\neg A \in Fin \to \exists y (y \subseteq A \land y \approx card (𝒫 n)))$
28		finnum	$⊢ 𝒫 n \in Fin \to 𝒫 n \in dom card$
29		cardid2	$⊢ 𝒫 n \in dom card \to card (𝒫 n) \approx 𝒫 n$
30		entr	$⊢ (y \approx card (𝒫 n) \land card (𝒫 n) \approx 𝒫 n) \to y \approx 𝒫 n$
31	30	expcom	$⊢ card (𝒫 n) \approx 𝒫 n \to (y \approx card (𝒫 n) \to y \approx 𝒫 n)$
32	19 28 29 31	4syl	$⊢ n \in ω \to (y \approx card (𝒫 n) \to y \approx 𝒫 n)$
33	32	anim2d	$⊢ n \in ω \to ((y \subseteq A \land y \approx card (𝒫 n)) \to (y \subseteq A \land y \approx 𝒫 n))$
34	33	eximdv	$⊢ n \in ω \to (\exists y (y \subseteq A \land y \approx card (𝒫 n)) \to \exists y (y \subseteq A \land y \approx 𝒫 n))$
35	27 34	syld	$⊢ n \in ω \to (\neg A \in Fin \to \exists y (y \subseteq A \land y \approx 𝒫 n))$
36	2	neeq1i	$⊢ B \neq \emptyset \leftrightarrow \{y \| (y \subseteq A \land y \approx 𝒫 n)\} \neq \emptyset$
37		abn0	$⊢ \{y \| (y \subseteq A \land y \approx 𝒫 n)\} \neq \emptyset \leftrightarrow \exists y (y \subseteq A \land y \approx 𝒫 n)$
38	36 37	bitri	$⊢ B \neq \emptyset \leftrightarrow \exists y (y \subseteq A \land y \approx 𝒫 n)$
39	35 38	imbitrrdi	$⊢ n \in ω \to (\neg A \in Fin \to B \neq \emptyset)$
40	39	com12	$⊢ \neg A \in Fin \to (n \in ω \to B \neq \emptyset)$
41	40	adantr	$⊢ (\neg A \in Fin \land \forall n \in ω (B \neq \emptyset \to b (n) \in B)) \to (n \in ω \to B \neq \emptyset)$
42		rsp	$⊢ \forall n \in ω (B \neq \emptyset \to b (n) \in B) \to (n \in ω \to (B \neq \emptyset \to b (n) \in B))$
43	42	adantl	$⊢ (\neg A \in Fin \land \forall n \in ω (B \neq \emptyset \to b (n) \in B)) \to (n \in ω \to (B \neq \emptyset \to b (n) \in B))$
44	41 43	mpdd	$⊢ (\neg A \in Fin \land \forall n \in ω (B \neq \emptyset \to b (n) \in B)) \to (n \in ω \to b (n) \in B)$
45	16 44	ralrimi	$⊢ (\neg A \in Fin \land \forall n \in ω (B \neq \emptyset \to b (n) \in B)) \to \forall n \in ω b (n) \in B$
46	45	3adant2	$⊢ (\neg A \in Fin \land b Fn ω \land \forall n \in ω (B \neq \emptyset \to b (n) \in B)) \to \forall n \in ω b (n) \in B$
47	46	3expib	$⊢ \neg A \in Fin \to ((b Fn ω \land \forall n \in ω (B \neq \emptyset \to b (n) \in B)) \to \forall n \in ω b (n) \in B)$
48	47	eximdv	$⊢ \neg A \in Fin \to (\exists b (b Fn ω \land \forall n \in ω (B \neq \emptyset \to b (n) \in B)) \to \exists b \forall n \in ω b (n) \in B)$
49	13 48	mpi	$⊢ \neg A \in Fin \to \exists b \forall n \in ω b (n) \in B$
50		axcc2	$⊢ \exists c (c Fn ω \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n)))$
51		simp2	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to c Fn ω$
52		nfra1	$⊢ Ⅎ n \forall n \in ω b (n) \in B$
53		nfra1	$⊢ Ⅎ n \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))$
54	52 53	nfan	$⊢ Ⅎ n (\forall n \in ω b (n) \in B \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n)))$
55		fvex	$⊢ b (n) \in V$
56		sseq1	$⊢ y = b (n) \to (y \subseteq A \leftrightarrow b (n) \subseteq A)$
57		breq1	$⊢ y = b (n) \to (y \approx 𝒫 n \leftrightarrow b (n) \approx 𝒫 n)$
58	56 57	anbi12d	$⊢ y = b (n) \to ((y \subseteq A \land y \approx 𝒫 n) \leftrightarrow (b (n) \subseteq A \land b (n) \approx 𝒫 n))$
59	55 58 2	elab2	$⊢ b (n) \in B \leftrightarrow (b (n) \subseteq A \land b (n) \approx 𝒫 n)$
60	59	simprbi	$⊢ b (n) \in B \to b (n) \approx 𝒫 n$
61	60	ralimi	$⊢ \forall n \in ω b (n) \in B \to \forall n \in ω b (n) \approx 𝒫 n$
62		fveq2	$⊢ n = k \to b (n) = b (k)$
63		pweq	$⊢ n = k \to 𝒫 n = 𝒫 k$
64	62 63	breq12d	$⊢ n = k \to (b (n) \approx 𝒫 n \leftrightarrow b (k) \approx 𝒫 k)$
65	64	cbvralvw	$⊢ \forall n \in ω b (n) \approx 𝒫 n \leftrightarrow \forall k \in ω b (k) \approx 𝒫 k$
66		peano2	$⊢ n \in ω \to suc n \in ω$
67		omelon	$⊢ ω \in On$
68	67	onelssi	$⊢ suc n \in ω \to suc n \subseteq ω$
69		ssralv	$⊢ suc n \subseteq ω \to (\forall k \in ω b (k) \approx 𝒫 k \to \forall k \in suc n b (k) \approx 𝒫 k)$
70	66 68 69	3syl	$⊢ n \in ω \to (\forall k \in ω b (k) \approx 𝒫 k \to \forall k \in suc n b (k) \approx 𝒫 k)$
71		pwsdompw	$⊢ (n \in ω \land \forall k \in suc n b (k) \approx 𝒫 k) \to ⋃_{k \in n} b (k) ≺ b (n)$
72	71	ex	$⊢ n \in ω \to (\forall k \in suc n b (k) \approx 𝒫 k \to ⋃_{k \in n} b (k) ≺ b (n))$
73	70 72	syld	$⊢ n \in ω \to (\forall k \in ω b (k) \approx 𝒫 k \to ⋃_{k \in n} b (k) ≺ b (n))$
74		sdomdif	$⊢ ⋃_{k \in n} b (k) ≺ b (n) \to b (n) ∖ ⋃_{k \in n} b (k) \neq \emptyset$
75	73 74	syl6	$⊢ n \in ω \to (\forall k \in ω b (k) \approx 𝒫 k \to b (n) ∖ ⋃_{k \in n} b (k) \neq \emptyset)$
76	65 75	biimtrid	$⊢ n \in ω \to (\forall n \in ω b (n) \approx 𝒫 n \to b (n) ∖ ⋃_{k \in n} b (k) \neq \emptyset)$
77	55	difexi	$⊢ b (n) ∖ ⋃_{k \in n} b (k) \in V$
78	3	fvmpt2	$⊢ (n \in ω \land b (n) ∖ ⋃_{k \in n} b (k) \in V) \to C (n) = b (n) ∖ ⋃_{k \in n} b (k)$
79	77 78	mpan2	$⊢ n \in ω \to C (n) = b (n) ∖ ⋃_{k \in n} b (k)$
80	79	neeq1d	$⊢ n \in ω \to (C (n) \neq \emptyset \leftrightarrow b (n) ∖ ⋃_{k \in n} b (k) \neq \emptyset)$
81	76 80	sylibrd	$⊢ n \in ω \to (\forall n \in ω b (n) \approx 𝒫 n \to C (n) \neq \emptyset)$
82	61 81	syl5com	$⊢ \forall n \in ω b (n) \in B \to (n \in ω \to C (n) \neq \emptyset)$
83	82	adantr	$⊢ (\forall n \in ω b (n) \in B \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to (n \in ω \to C (n) \neq \emptyset)$
84		rsp	$⊢ \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n)) \to (n \in ω \to (C (n) \neq \emptyset \to c (n) \in C (n)))$
85	84	adantl	$⊢ (\forall n \in ω b (n) \in B \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to (n \in ω \to (C (n) \neq \emptyset \to c (n) \in C (n)))$
86	83 85	mpdd	$⊢ (\forall n \in ω b (n) \in B \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to (n \in ω \to c (n) \in C (n))$
87	54 86	ralrimi	$⊢ (\forall n \in ω b (n) \in B \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to \forall n \in ω c (n) \in C (n)$
88	87	3adant2	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to \forall n \in ω c (n) \in C (n)$
89	51 88	jca	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to (c Fn ω \land \forall n \in ω c (n) \in C (n))$
90	89	3expib	$⊢ \forall n \in ω b (n) \in B \to ((c Fn ω \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to (c Fn ω \land \forall n \in ω c (n) \in C (n)))$
91	90	eximdv	$⊢ \forall n \in ω b (n) \in B \to (\exists c (c Fn ω \land \forall n \in ω (C (n) \neq \emptyset \to c (n) \in C (n))) \to \exists c (c Fn ω \land \forall n \in ω c (n) \in C (n)))$
92	50 91	mpi	$⊢ \forall n \in ω b (n) \in B \to \exists c (c Fn ω \land \forall n \in ω c (n) \in C (n))$
93		simp2	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω c (n) \in C (n)) \to c Fn ω$
94		nfra1	$⊢ Ⅎ n \forall n \in ω c (n) \in C (n)$
95	52 94	nfan	$⊢ Ⅎ n (\forall n \in ω b (n) \in B \land \forall n \in ω c (n) \in C (n))$
96		rsp	$⊢ \forall n \in ω c (n) \in C (n) \to (n \in ω \to c (n) \in C (n))$
97	96	com12	$⊢ n \in ω \to (\forall n \in ω c (n) \in C (n) \to c (n) \in C (n))$
98		rsp	$⊢ \forall n \in ω b (n) \in B \to (n \in ω \to b (n) \in B)$
99	98	com12	$⊢ n \in ω \to (\forall n \in ω b (n) \in B \to b (n) \in B)$
100	79	eleq2d	$⊢ n \in ω \to (c (n) \in C (n) \leftrightarrow c (n) \in (b (n) ∖ ⋃_{k \in n} b (k)))$
101		eldifi	$⊢ c (n) \in (b (n) ∖ ⋃_{k \in n} b (k)) \to c (n) \in b (n)$
102	100 101	biimtrdi	$⊢ n \in ω \to (c (n) \in C (n) \to c (n) \in b (n))$
103	59	simplbi	$⊢ b (n) \in B \to b (n) \subseteq A$
104	103	sseld	$⊢ b (n) \in B \to (c (n) \in b (n) \to c (n) \in A)$
105	102 104	syl9	$⊢ n \in ω \to (b (n) \in B \to (c (n) \in C (n) \to c (n) \in A))$
106	99 105	syld	$⊢ n \in ω \to (\forall n \in ω b (n) \in B \to (c (n) \in C (n) \to c (n) \in A))$
107	106	com23	$⊢ n \in ω \to (c (n) \in C (n) \to (\forall n \in ω b (n) \in B \to c (n) \in A))$
108	97 107	syld	$⊢ n \in ω \to (\forall n \in ω c (n) \in C (n) \to (\forall n \in ω b (n) \in B \to c (n) \in A))$
109	108	com13	$⊢ \forall n \in ω b (n) \in B \to (\forall n \in ω c (n) \in C (n) \to (n \in ω \to c (n) \in A))$
110	109	imp	$⊢ (\forall n \in ω b (n) \in B \land \forall n \in ω c (n) \in C (n)) \to (n \in ω \to c (n) \in A)$
111	95 110	ralrimi	$⊢ (\forall n \in ω b (n) \in B \land \forall n \in ω c (n) \in C (n)) \to \forall n \in ω c (n) \in A$
112	111	3adant2	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω c (n) \in C (n)) \to \forall n \in ω c (n) \in A$
113		ffnfv	$⊢ c : ω ⟶ A \leftrightarrow (c Fn ω \land \forall n \in ω c (n) \in A)$
114	93 112 113	sylanbrc	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω c (n) \in C (n)) \to c : ω ⟶ A$
115		nfv	$⊢ Ⅎ n k \in ω$
116		nnord	$⊢ k \in ω \to Ord k$
117		nnord	$⊢ n \in ω \to Ord n$
118		ordtri3or	$⊢ (Ord k \land Ord n) \to (k \in n \lor k = n \lor n \in k)$
119	116 117 118	syl2an	$⊢ (k \in ω \land n \in ω) \to (k \in n \lor k = n \lor n \in k)$
120		fveq2	$⊢ n = k \to c (n) = c (k)$
121		fveq2	$⊢ k = j \to b (k) = b (j)$
122	121	cbviunv	$⊢ ⋃_{k \in n} b (k) = ⋃_{j \in n} b (j)$
123		iuneq1	$⊢ n = k \to ⋃_{j \in n} b (j) = ⋃_{j \in k} b (j)$
124	122 123	eqtrid	$⊢ n = k \to ⋃_{k \in n} b (k) = ⋃_{j \in k} b (j)$
125	62 124	difeq12d	$⊢ n = k \to b (n) ∖ ⋃_{k \in n} b (k) = b (k) ∖ ⋃_{j \in k} b (j)$
126	120 125	eleq12d	$⊢ n = k \to (c (n) \in (b (n) ∖ ⋃_{k \in n} b (k)) \leftrightarrow c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)))$
127	126	rspccv	$⊢ \forall n \in ω c (n) \in (b (n) ∖ ⋃_{k \in n} b (k)) \to (k \in ω \to c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)))$
128	96 100	mpbidi	$⊢ \forall n \in ω c (n) \in C (n) \to (n \in ω \to c (n) \in (b (n) ∖ ⋃_{k \in n} b (k)))$
129	94 128	ralrimi	$⊢ \forall n \in ω c (n) \in C (n) \to \forall n \in ω c (n) \in (b (n) ∖ ⋃_{k \in n} b (k))$
130	127 129	syl11	$⊢ k \in ω \to (\forall n \in ω c (n) \in C (n) \to c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)))$
131	130	3ad2ant1	$⊢ (k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)))$
132		eldifi	$⊢ c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)) \to c (k) \in b (k)$
133		eleq1	$⊢ c (k) = c (n) \to (c (k) \in b (k) \leftrightarrow c (n) \in b (k))$
134	132 133	imbitrid	$⊢ c (k) = c (n) \to (c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)) \to c (n) \in b (k))$
135	134	3ad2ant3	$⊢ (k \in ω \land n \in ω \land c (k) = c (n)) \to (c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)) \to c (n) \in b (k))$
136	131 135	syld	$⊢ (k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to c (n) \in b (k))$
137	136	imp	$⊢ ((k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to c (n) \in b (k)$
138		ssiun2	$⊢ k \in n \to b (k) \subseteq ⋃_{k \in n} b (k)$
139	138	sseld	$⊢ k \in n \to (c (n) \in b (k) \to c (n) \in ⋃_{k \in n} b (k))$
140	137 139	syl5	$⊢ k \in n \to (((k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to c (n) \in ⋃_{k \in n} b (k))$
141	140	3impib	$⊢ (k \in n \land (k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to c (n) \in ⋃_{k \in n} b (k)$
142	128	com12	$⊢ n \in ω \to (\forall n \in ω c (n) \in C (n) \to c (n) \in (b (n) ∖ ⋃_{k \in n} b (k)))$
143	142	3ad2ant2	$⊢ (k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to c (n) \in (b (n) ∖ ⋃_{k \in n} b (k)))$
144	143	imp	$⊢ ((k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to c (n) \in (b (n) ∖ ⋃_{k \in n} b (k))$
145	144	eldifbd	$⊢ ((k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to \neg c (n) \in ⋃_{k \in n} b (k)$
146	145	3adant1	$⊢ (k \in n \land (k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to \neg c (n) \in ⋃_{k \in n} b (k)$
147	141 146	pm2.21dd	$⊢ (k \in n \land (k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to k = n$
148	147	3exp	$⊢ k \in n \to ((k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to k = n))$
149		2a1	$⊢ k = n \to ((k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to k = n))$
150		fveq2	$⊢ j = n \to b (j) = b (n)$
151	150	ssiun2s	$⊢ n \in k \to b (n) \subseteq ⋃_{j \in k} b (j)$
152	151	sseld	$⊢ n \in k \to (c (n) \in b (n) \to c (n) \in ⋃_{j \in k} b (j))$
153	101 152	syl5	$⊢ n \in k \to (c (n) \in (b (n) ∖ ⋃_{k \in n} b (k)) \to c (n) \in ⋃_{j \in k} b (j))$
154	144 153	syl5	$⊢ n \in k \to (((k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to c (n) \in ⋃_{j \in k} b (j))$
155	154	3impib	$⊢ (n \in k \land (k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to c (n) \in ⋃_{j \in k} b (j)$
156		eleq1	$⊢ c (k) = c (n) \to (c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)) \leftrightarrow c (n) \in (b (k) ∖ ⋃_{j \in k} b (j)))$
157		eldifn	$⊢ c (n) \in (b (k) ∖ ⋃_{j \in k} b (j)) \to \neg c (n) \in ⋃_{j \in k} b (j)$
158	156 157	biimtrdi	$⊢ c (k) = c (n) \to (c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)) \to \neg c (n) \in ⋃_{j \in k} b (j))$
159	158	3ad2ant3	$⊢ (k \in ω \land n \in ω \land c (k) = c (n)) \to (c (k) \in (b (k) ∖ ⋃_{j \in k} b (j)) \to \neg c (n) \in ⋃_{j \in k} b (j))$
160	131 159	syld	$⊢ (k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to \neg c (n) \in ⋃_{j \in k} b (j))$
161	160	a1i	$⊢ n \in k \to ((k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to \neg c (n) \in ⋃_{j \in k} b (j)))$
162	161	3imp	$⊢ (n \in k \land (k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to \neg c (n) \in ⋃_{j \in k} b (j)$
163	155 162	pm2.21dd	$⊢ (n \in k \land (k \in ω \land n \in ω \land c (k) = c (n)) \land \forall n \in ω c (n) \in C (n)) \to k = n$
164	163	3exp	$⊢ n \in k \to ((k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to k = n))$
165	148 149 164	3jaoi	$⊢ (k \in n \lor k = n \lor n \in k) \to ((k \in ω \land n \in ω \land c (k) = c (n)) \to (\forall n \in ω c (n) \in C (n) \to k = n))$
166	165	com12	$⊢ (k \in ω \land n \in ω \land c (k) = c (n)) \to ((k \in n \lor k = n \lor n \in k) \to (\forall n \in ω c (n) \in C (n) \to k = n))$
167	166	3expia	$⊢ (k \in ω \land n \in ω) \to (c (k) = c (n) \to ((k \in n \lor k = n \lor n \in k) \to (\forall n \in ω c (n) \in C (n) \to k = n)))$
168	119 167	mpid	$⊢ (k \in ω \land n \in ω) \to (c (k) = c (n) \to (\forall n \in ω c (n) \in C (n) \to k = n))$
169	168	com3r	$⊢ \forall n \in ω c (n) \in C (n) \to ((k \in ω \land n \in ω) \to (c (k) = c (n) \to k = n))$
170	169	expd	$⊢ \forall n \in ω c (n) \in C (n) \to (k \in ω \to (n \in ω \to (c (k) = c (n) \to k = n)))$
171	94 115 170	ralrimd	$⊢ \forall n \in ω c (n) \in C (n) \to (k \in ω \to \forall n \in ω (c (k) = c (n) \to k = n))$
172	171	ralrimiv	$⊢ \forall n \in ω c (n) \in C (n) \to \forall k \in ω \forall n \in ω (c (k) = c (n) \to k = n)$
173	172	3ad2ant3	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω c (n) \in C (n)) \to \forall k \in ω \forall n \in ω (c (k) = c (n) \to k = n)$
174		dff13	$⊢ c : ω \underset{1-1}{⟶} A \leftrightarrow (c : ω ⟶ A \land \forall k \in ω \forall n \in ω (c (k) = c (n) \to k = n))$
175	114 173 174	sylanbrc	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω c (n) \in C (n)) \to c : ω \underset{1-1}{⟶} A$
176	175	19.8ad	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω c (n) \in C (n)) \to \exists c c : ω \underset{1-1}{⟶} A$
177	1	brdom	$⊢ ω ≼ A \leftrightarrow \exists c c : ω \underset{1-1}{⟶} A$
178	176 177	sylibr	$⊢ (\forall n \in ω b (n) \in B \land c Fn ω \land \forall n \in ω c (n) \in C (n)) \to ω ≼ A$
179	178	3expib	$⊢ \forall n \in ω b (n) \in B \to ((c Fn ω \land \forall n \in ω c (n) \in C (n)) \to ω ≼ A)$
180	179	exlimdv	$⊢ \forall n \in ω b (n) \in B \to (\exists c (c Fn ω \land \forall n \in ω c (n) \in C (n)) \to ω ≼ A)$
181	92 180	mpd	$⊢ \forall n \in ω b (n) \in B \to ω ≼ A$
182	181	exlimiv	$⊢ \exists b \forall n \in ω b (n) \in B \to ω ≼ A$
183	49 182	syl	$⊢ \neg A \in Fin \to ω ≼ A$

Metamath Proof Explorer

Theorem domtriomlem

Proof