Theorem cfpwsdom

Description: A corollary of Konig's Theorem konigth . Theorem 11.29 of TakeutiZaring p. 108. (Contributed by Mario Carneiro, 20-Mar-2013)

	Ref	Expression
Hypothesis	cfpwsdom.1	$$⊢B\in \mathrm{V}$$
Assertion	cfpwsdom	$$⊢2_{𝑜}\preccurlyeq B\to \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cfpwsdom.1	$$⊢B\in \mathrm{V}$$
2		ovex	$$⊢B^{\aleph \left(A\right)}\in \mathrm{V}$$
3	2	cardid	$$⊢\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\approx \left(B^{\aleph \left(A\right)}\right)$$
4	3	ensymi	$$⊢\left(B^{\aleph \left(A\right)}\right)\approx \mathrm{card}\left(B^{\aleph \left(A\right)}\right)$$
5		fvex	$$⊢\aleph \left(A\right)\in \mathrm{V}$$
6	5	canth2	$$⊢\aleph \left(A\right)\prec 𝒫\aleph \left(A\right)$$
7	5	pw2en	$$⊢𝒫\aleph \left(A\right)\approx \left({2_{𝑜}}^{\aleph \left(A\right)}\right)$$
8		sdomentr	$$⊢\left(\aleph \left(A\right)\prec 𝒫\aleph \left(A\right)\wedge 𝒫\aleph \left(A\right)\approx \left({2_{𝑜}}^{\aleph \left(A\right)}\right)\right)\to \aleph \left(A\right)\prec \left({2_{𝑜}}^{\aleph \left(A\right)}\right)$$
9	6 7 8	mp2an	$$⊢\aleph \left(A\right)\prec \left({2_{𝑜}}^{\aleph \left(A\right)}\right)$$
10		mapdom1	$$⊢2_{𝑜}\preccurlyeq B\to \left({2_{𝑜}}^{\aleph \left(A\right)}\right)\preccurlyeq \left(B^{\aleph \left(A\right)}\right)$$
11		sdomdomtr	$$⊢\left(\aleph \left(A\right)\prec \left({2_{𝑜}}^{\aleph \left(A\right)}\right)\wedge \left({2_{𝑜}}^{\aleph \left(A\right)}\right)\preccurlyeq \left(B^{\aleph \left(A\right)}\right)\right)\to \aleph \left(A\right)\prec \left(B^{\aleph \left(A\right)}\right)$$
12	9 10 11	sylancr	$$⊢2_{𝑜}\preccurlyeq B\to \aleph \left(A\right)\prec \left(B^{\aleph \left(A\right)}\right)$$
13		ficard	$$⊢B^{\aleph \left(A\right)}\in \mathrm{V}\to \left(B^{\aleph \left(A\right)}\in \mathrm{Fin}\leftrightarrow \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\right)$$
14	2 13	ax-mp	$$⊢B^{\aleph \left(A\right)}\in \mathrm{Fin}\leftrightarrow \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }$$
15		fict	$$⊢B^{\aleph \left(A\right)}\in \mathrm{Fin}\to \left(B^{\aleph \left(A\right)}\right)\preccurlyeq \mathrm{\omega }$$
16	14 15	sylbir	$$⊢\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\to \left(B^{\aleph \left(A\right)}\right)\preccurlyeq \mathrm{\omega }$$
17		alephgeom	$$⊢A\in \mathrm{On}\leftrightarrow \mathrm{\omega }\subseteq \aleph \left(A\right)$$
18		alephon	$$⊢\aleph \left(A\right)\in \mathrm{On}$$
19		ssdomg	$$⊢\aleph \left(A\right)\in \mathrm{On}\to \left(\mathrm{\omega }\subseteq \aleph \left(A\right)\to \mathrm{\omega }\preccurlyeq \aleph \left(A\right)\right)$$
20	18 19	ax-mp	$$⊢\mathrm{\omega }\subseteq \aleph \left(A\right)\to \mathrm{\omega }\preccurlyeq \aleph \left(A\right)$$
21	17 20	sylbi	$$⊢A\in \mathrm{On}\to \mathrm{\omega }\preccurlyeq \aleph \left(A\right)$$
22		domtr	$$⊢\left(\left(B^{\aleph \left(A\right)}\right)\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\preccurlyeq \aleph \left(A\right)\right)\to \left(B^{\aleph \left(A\right)}\right)\preccurlyeq \aleph \left(A\right)$$
23	16 21 22	syl2an	$$⊢\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\wedge A\in \mathrm{On}\right)\to \left(B^{\aleph \left(A\right)}\right)\preccurlyeq \aleph \left(A\right)$$
24		domnsym	$$⊢\left(B^{\aleph \left(A\right)}\right)\preccurlyeq \aleph \left(A\right)\to \neg \aleph \left(A\right)\prec \left(B^{\aleph \left(A\right)}\right)$$
25	23 24	syl	$$⊢\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\wedge A\in \mathrm{On}\right)\to \neg \aleph \left(A\right)\prec \left(B^{\aleph \left(A\right)}\right)$$
26	25	expcom	$$⊢A\in \mathrm{On}\to \left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\to \neg \aleph \left(A\right)\prec \left(B^{\aleph \left(A\right)}\right)\right)$$
27	26	con2d	$$⊢A\in \mathrm{On}\to \left(\aleph \left(A\right)\prec \left(B^{\aleph \left(A\right)}\right)\to \neg \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\right)$$
28		cardidm	$$⊢\mathrm{card}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)$$
29		iscard3	$$⊢\mathrm{card}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\leftrightarrow \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)$$
30		elun	$$⊢\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)\leftrightarrow \left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\vee \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{ran}\aleph \right)$$
31		df-or	$$⊢\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\vee \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{ran}\aleph \right)\leftrightarrow \left(\neg \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{ran}\aleph \right)$$
32	29 30 31	3bitri	$$⊢\mathrm{card}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\leftrightarrow \left(\neg \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{ran}\aleph \right)$$
33	28 32	mpbi	$$⊢\neg \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{\omega }\to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{ran}\aleph$$
34	12 27 33	syl56	$$⊢A\in \mathrm{On}\to \left(2_{𝑜}\preccurlyeq B\to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{ran}\aleph \right)$$
35		alephfnon	$$⊢\aleph Fn\mathrm{On}$$
36		fvelrnb	$$⊢\aleph Fn\mathrm{On}\to \left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{ran}\aleph \leftrightarrow \exists x\in \mathrm{On}\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$
37	35 36	ax-mp	$$⊢\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\in \mathrm{ran}\aleph \leftrightarrow \exists x\in \mathrm{On}\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)$$
38	34 37	syl6ib	$$⊢A\in \mathrm{On}\to \left(2_{𝑜}\preccurlyeq B\to \exists x\in \mathrm{On}\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$
39		eqid	$$⊢\left(y\in \mathrm{cf}\left(\aleph \left(x\right)\right)⟼\mathrm{har}\left(z\left(y\right)\right)\right)=\left(y\in \mathrm{cf}\left(\aleph \left(x\right)\right)⟼\mathrm{har}\left(z\left(y\right)\right)\right)$$
40	39	pwcfsdom	$$⊢\aleph \left(x\right)\prec \left({\aleph \left(x\right)}^{\mathrm{cf}\left(\aleph \left(x\right)\right)}\right)$$
41		id	$$⊢\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\to \aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)$$
42		fveq2	$$⊢\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\to \mathrm{cf}\left(\aleph \left(x\right)\right)=\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$
43	41 42	oveq12d	$$⊢\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\to {\aleph \left(x\right)}^{\mathrm{cf}\left(\aleph \left(x\right)\right)}={\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}$$
44	41 43	breq12d	$$⊢\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\to \left(\aleph \left(x\right)\prec \left({\aleph \left(x\right)}^{\mathrm{cf}\left(\aleph \left(x\right)\right)}\right)\leftrightarrow \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\right)$$
45	40 44	mpbii	$$⊢\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)$$
46	45	rexlimivw	$$⊢\exists x\in \mathrm{On}\aleph \left(x\right)=\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)$$
47	38 46	syl6	$$⊢A\in \mathrm{On}\to \left(2_{𝑜}\preccurlyeq B\to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\right)$$
48	47	imp	$$⊢\left(A\in \mathrm{On}\wedge 2_{𝑜}\preccurlyeq B\right)\to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)$$
49		ensdomtr	$$⊢\left(\left(B^{\aleph \left(A\right)}\right)\approx \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\wedge \mathrm{card}\left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\right)\to \left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)$$
50	4 48 49	sylancr	$$⊢\left(A\in \mathrm{On}\wedge 2_{𝑜}\preccurlyeq B\right)\to \left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)$$
51		fvex	$$⊢\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\in \mathrm{V}$$
52	51	enref	$$⊢\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\approx \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$
53		mapen	$$⊢\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\approx \left(B^{\aleph \left(A\right)}\right)\wedge \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\approx \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)\to \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\approx \left({\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)$$
54	3 52 53	mp2an	$$⊢\left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\approx \left({\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)$$
55		mapxpen	$$⊢\left(B\in \mathrm{V}\wedge \aleph \left(A\right)\in \mathrm{On}\wedge \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\in \mathrm{V}\right)\to \left({\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\approx \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)$$
56	1 18 51 55	mp3an	$$⊢\left({\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\approx \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)$$
57	54 56	entri	$$⊢\left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\approx \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)$$
58		sdomentr	$$⊢\left(\left(B^{\aleph \left(A\right)}\right)\prec \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\wedge \left({\mathrm{card}\left(B^{\aleph \left(A\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)}\right)\approx \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)\right)\to \left(B^{\aleph \left(A\right)}\right)\prec \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)$$
59	50 57 58	sylancl	$$⊢\left(A\in \mathrm{On}\wedge 2_{𝑜}\preccurlyeq B\right)\to \left(B^{\aleph \left(A\right)}\right)\prec \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)$$
60	5	xpdom2	$$⊢\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)\to \left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)\preccurlyeq \left(\aleph \left(A\right)\times \aleph \left(A\right)\right)$$
61	17	biimpi	$$⊢A\in \mathrm{On}\to \mathrm{\omega }\subseteq \aleph \left(A\right)$$
62		infxpen	$$⊢\left(\aleph \left(A\right)\in \mathrm{On}\wedge \mathrm{\omega }\subseteq \aleph \left(A\right)\right)\to \left(\aleph \left(A\right)\times \aleph \left(A\right)\right)\approx \aleph \left(A\right)$$
63	18 61 62	sylancr	$$⊢A\in \mathrm{On}\to \left(\aleph \left(A\right)\times \aleph \left(A\right)\right)\approx \aleph \left(A\right)$$
64		domentr	$$⊢\left(\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)\preccurlyeq \left(\aleph \left(A\right)\times \aleph \left(A\right)\right)\wedge \left(\aleph \left(A\right)\times \aleph \left(A\right)\right)\approx \aleph \left(A\right)\right)\to \left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)\preccurlyeq \aleph \left(A\right)$$
65	60 63 64	syl2an	$$⊢\left(\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)\wedge A\in \mathrm{On}\right)\to \left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)\preccurlyeq \aleph \left(A\right)$$
66		nsuceq0	$$⊢\mathrm{suc}{1}_{𝑜}\ne \varnothing$$
67		dom0	$$⊢\mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \leftrightarrow \mathrm{suc}{1}_{𝑜}=\varnothing$$
68	66 67	nemtbir	$$⊢\neg \mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing$$
69		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
70	69	breq1i	$$⊢2_{𝑜}\preccurlyeq B\leftrightarrow \mathrm{suc}{1}_{𝑜}\preccurlyeq B$$
71		breq2	$$⊢B=\varnothing \to \left(\mathrm{suc}{1}_{𝑜}\preccurlyeq B\leftrightarrow \mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \right)$$
72	70 71	syl5bb	$$⊢B=\varnothing \to \left(2_{𝑜}\preccurlyeq B\leftrightarrow \mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \right)$$
73	72	biimpcd	$$⊢2_{𝑜}\preccurlyeq B\to \left(B=\varnothing \to \mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \right)$$
74	73	adantld	$$⊢2_{𝑜}\preccurlyeq B\to \left(\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)=\varnothing \wedge B=\varnothing \right)\to \mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \right)$$
75	68 74	mtoi	$$⊢2_{𝑜}\preccurlyeq B\to \neg \left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)=\varnothing \wedge B=\varnothing \right)$$
76		mapdom2	$$⊢\left(\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)\preccurlyeq \aleph \left(A\right)\wedge \neg \left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)=\varnothing \wedge B=\varnothing \right)\right)\to \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)\preccurlyeq \left(B^{\aleph \left(A\right)}\right)$$
77	65 75 76	syl2an	$$⊢\left(\left(\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)\wedge A\in \mathrm{On}\right)\wedge 2_{𝑜}\preccurlyeq B\right)\to \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)\preccurlyeq \left(B^{\aleph \left(A\right)}\right)$$
78		domnsym	$$⊢\left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)\preccurlyeq \left(B^{\aleph \left(A\right)}\right)\to \neg \left(B^{\aleph \left(A\right)}\right)\prec \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)$$
79	77 78	syl	$$⊢\left(\left(\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)\wedge A\in \mathrm{On}\right)\wedge 2_{𝑜}\preccurlyeq B\right)\to \neg \left(B^{\aleph \left(A\right)}\right)\prec \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)$$
80	79	expl	$$⊢\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)\to \left(\left(A\in \mathrm{On}\wedge 2_{𝑜}\preccurlyeq B\right)\to \neg \left(B^{\aleph \left(A\right)}\right)\prec \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)\right)$$
81	80	com12	$$⊢\left(A\in \mathrm{On}\wedge 2_{𝑜}\preccurlyeq B\right)\to \left(\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)\to \neg \left(B^{\aleph \left(A\right)}\right)\prec \left(B^{\left(\aleph \left(A\right)\times \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)}\right)\right)$$
82	59 81	mt2d	$$⊢\left(A\in \mathrm{On}\wedge 2_{𝑜}\preccurlyeq B\right)\to \neg \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)$$
83		domtri	$$⊢\left(\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\in \mathrm{V}\wedge \aleph \left(A\right)\in \mathrm{V}\right)\to \left(\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)\leftrightarrow \neg \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)$$
84	51 5 83	mp2an	$$⊢\mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)\leftrightarrow \neg \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$
85	84	biimpri	$$⊢\neg \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\to \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\preccurlyeq \aleph \left(A\right)$$
86	82 85	nsyl2	$$⊢\left(A\in \mathrm{On}\wedge 2_{𝑜}\preccurlyeq B\right)\to \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$
87	86	ex	$$⊢A\in \mathrm{On}\to \left(2_{𝑜}\preccurlyeq B\to \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)$$
88		fndm	$$⊢\aleph Fn\mathrm{On}\to \mathrm{dom}\aleph =\mathrm{On}$$
89	35 88	ax-mp	$$⊢\mathrm{dom}\aleph =\mathrm{On}$$
90	89	eleq2i	$$⊢A\in \mathrm{dom}\aleph \leftrightarrow A\in \mathrm{On}$$
91		ndmfv	$$⊢\neg A\in \mathrm{dom}\aleph \to \aleph \left(A\right)=\varnothing$$
92	90 91	sylnbir	$$⊢\neg A\in \mathrm{On}\to \aleph \left(A\right)=\varnothing$$
93		1n0	$$⊢1_{𝑜}\ne \varnothing$$
94		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
95	94	0sdom	$$⊢\varnothing \prec 1_{𝑜}\leftrightarrow 1_{𝑜}\ne \varnothing$$
96	93 95	mpbir	$$⊢\varnothing \prec 1_{𝑜}$$
97		id	$$⊢\aleph \left(A\right)=\varnothing \to \aleph \left(A\right)=\varnothing$$
98		oveq2	$$⊢\aleph \left(A\right)=\varnothing \to B^{\aleph \left(A\right)}=B^{\varnothing }$$
99		map0e	$$⊢B\in \mathrm{V}\to B^{\varnothing }=1_{𝑜}$$
100	1 99	ax-mp	$$⊢B^{\varnothing }=1_{𝑜}$$
101	98 100	eqtrdi	$$⊢\aleph \left(A\right)=\varnothing \to B^{\aleph \left(A\right)}=1_{𝑜}$$
102	101	fveq2d	$$⊢\aleph \left(A\right)=\varnothing \to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)=\mathrm{card}\left(1_{𝑜}\right)$$
103		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
104		cardnn	$$⊢1_{𝑜}\in \mathrm{\omega }\to \mathrm{card}\left(1_{𝑜}\right)=1_{𝑜}$$
105	103 104	ax-mp	$$⊢\mathrm{card}\left(1_{𝑜}\right)=1_{𝑜}$$
106	102 105	eqtrdi	$$⊢\aleph \left(A\right)=\varnothing \to \mathrm{card}\left(B^{\aleph \left(A\right)}\right)=1_{𝑜}$$
107	106	fveq2d	$$⊢\aleph \left(A\right)=\varnothing \to \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)=\mathrm{cf}\left(1_{𝑜}\right)$$
108		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
109	108	fveq2i	$$⊢\mathrm{cf}\left(1_{𝑜}\right)=\mathrm{cf}\left(\mathrm{suc}\varnothing \right)$$
110		0elon	$$⊢\varnothing \in \mathrm{On}$$
111		cfsuc	$$⊢\varnothing \in \mathrm{On}\to \mathrm{cf}\left(\mathrm{suc}\varnothing \right)=1_{𝑜}$$
112	110 111	ax-mp	$$⊢\mathrm{cf}\left(\mathrm{suc}\varnothing \right)=1_{𝑜}$$
113	109 112	eqtri	$$⊢\mathrm{cf}\left(1_{𝑜}\right)=1_{𝑜}$$
114	107 113	eqtrdi	$$⊢\aleph \left(A\right)=\varnothing \to \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)=1_{𝑜}$$
115	97 114	breq12d	$$⊢\aleph \left(A\right)=\varnothing \to \left(\aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\leftrightarrow \varnothing \prec 1_{𝑜}\right)$$
116	96 115	mpbiri	$$⊢\aleph \left(A\right)=\varnothing \to \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$
117	116	a1d	$$⊢\aleph \left(A\right)=\varnothing \to \left(2_{𝑜}\preccurlyeq B\to \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)$$
118	92 117	syl	$$⊢\neg A\in \mathrm{On}\to \left(2_{𝑜}\preccurlyeq B\to \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)\right)$$
119	87 118	pm2.61i	$$⊢2_{𝑜}\preccurlyeq B\to \aleph \left(A\right)\prec \mathrm{cf}\left(\mathrm{card}\left(B^{\aleph \left(A\right)}\right)\right)$$