Theorem j0ltaleph

Description: The value of _J0 is less than an aleph if its two arguments are less than that aleph. Proposition 15.1(2) of TakeutiZaring p. 154. (Contributed by BTernaryTau, 25-Sep-2026)

	Ref	Expression
Assertion	j0ltaleph	Could not format assertion : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
2		j0iso	Could not format _J0 Isom _R0 , _E ( ( On X. On ) , On ) : No typesetting found for |- _J0 Isom _R0 , _E ( ( On X. On ) , On ) with typecode |-
3		isof1o	Could not format ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On ) : No typesetting found for |- ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On ) with typecode |-
4		f1of	Could not format ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On ) : No typesetting found for |- ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On ) with typecode |-
5	2 3 4	mp2b	Could not format _J0 : ( On X. On ) --> On : No typesetting found for |- _J0 : ( On X. On ) --> On with typecode |-
6		0elon	$$⊢\varnothing \in \mathrm{On}$$
7	5 6	f0cli	Could not format ( _J0 ` <. A , B >. ) e. On : No typesetting found for |- ( _J0 ` <. A , B >. ) e. On with typecode |-
8		domtriord	Could not format ( ( _om e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) <-> -. ( _J0 ` <. A , B >. ) ~< _om ) ) : No typesetting found for |- ( ( _om e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) <-> -. ( _J0 ` <. A , B >. ) ~< _om ) ) with typecode |-
9	1 7 8	mp2an	Could not format ( _om ~<_ ( _J0 ` <. A , B >. ) <-> -. ( _J0 ` <. A , B >. ) ~< _om ) : No typesetting found for |- ( _om ~<_ ( _J0 ` <. A , B >. ) <-> -. ( _J0 ` <. A , B >. ) ~< _om ) with typecode |-
10	9	con2bii	Could not format ( ( _J0 ` <. A , B >. ) ~< _om <-> -. _om ~<_ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) ~< _om <-> -. _om ~<_ ( _J0 ` <. A , B >. ) ) with typecode |-
11		sdomel	Could not format ( ( ( _J0 ` <. A , B >. ) e. On /\ _om e. On ) -> ( ( _J0 ` <. A , B >. ) ~< _om -> ( _J0 ` <. A , B >. ) e. _om ) ) : No typesetting found for |- ( ( ( _J0 ` <. A , B >. ) e. On /\ _om e. On ) -> ( ( _J0 ` <. A , B >. ) ~< _om -> ( _J0 ` <. A , B >. ) e. _om ) ) with typecode |-
12	7 1 11	mp2an	Could not format ( ( _J0 ` <. A , B >. ) ~< _om -> ( _J0 ` <. A , B >. ) e. _om ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) ~< _om -> ( _J0 ` <. A , B >. ) e. _om ) with typecode |-
13	10 12	sylbir	Could not format ( -. _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) e. _om ) : No typesetting found for |- ( -. _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) e. _om ) with typecode |-
14	13	orri	Could not format ( _om ~<_ ( _J0 ` <. A , B >. ) \/ ( _J0 ` <. A , B >. ) e. _om ) : No typesetting found for |- ( _om ~<_ ( _J0 ` <. A , B >. ) \/ ( _J0 ` <. A , B >. ) e. _om ) with typecode |-
15		alephon	$$⊢\aleph \left(C\right)\in \mathrm{On}$$
16	15	oneli	$$⊢A\in \aleph \left(C\right)\to A\in \mathrm{On}$$
17	15	oneli	$$⊢B\in \aleph \left(C\right)\to B\in \mathrm{On}$$
18	16 17	anim12i	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\right)\to \left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)$$
19	18	3adant3	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\wedge C\in \mathrm{On}\right)\to \left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)$$
20		j0ltalephlem	Could not format ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) with typecode |-
21		xpfi	$$⊢\left(\mathrm{suc}\left(A\cup B\right)\in \mathrm{Fin}\wedge \mathrm{suc}\left(A\cup B\right)\in \mathrm{Fin}\right)\to \mathrm{suc}\left(A\cup B\right)\times \mathrm{suc}\left(A\cup B\right)\in \mathrm{Fin}$$
22	21	anidms	$$⊢\mathrm{suc}\left(A\cup B\right)\in \mathrm{Fin}\to \mathrm{suc}\left(A\cup B\right)\times \mathrm{suc}\left(A\cup B\right)\in \mathrm{Fin}$$
23		domfi	Could not format ( ( ( suc ( A u. B ) X. suc ( A u. B ) ) e. Fin /\ ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) e. Fin ) : No typesetting found for |- ( ( ( suc ( A u. B ) X. suc ( A u. B ) ) e. Fin /\ ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) e. Fin ) with typecode |-
24	22 23	sylan	Could not format ( ( suc ( A u. B ) e. Fin /\ ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) e. Fin ) : No typesetting found for |- ( ( suc ( A u. B ) e. Fin /\ ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) e. Fin ) with typecode |-
25	24	expcom	Could not format ( ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) -> ( suc ( A u. B ) e. Fin -> ( _J0 ` <. A , B >. ) e. Fin ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) -> ( suc ( A u. B ) e. Fin -> ( _J0 ` <. A , B >. ) e. Fin ) ) with typecode |-
26	20 25	syl	Could not format ( ( A e. On /\ B e. On ) -> ( suc ( A u. B ) e. Fin -> ( _J0 ` <. A , B >. ) e. Fin ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( suc ( A u. B ) e. Fin -> ( _J0 ` <. A , B >. ) e. Fin ) ) with typecode |-
27		onenon	Could not format ( ( _J0 ` <. A , B >. ) e. On -> ( _J0 ` <. A , B >. ) e. dom card ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. On -> ( _J0 ` <. A , B >. ) e. dom card ) with typecode |-
28		infinfnum	Could not format ( ( _J0 ` <. A , B >. ) e. dom card -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. dom card -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) ) with typecode |-
29	7 27 28	mp2b	Could not format ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) with typecode |-
30	29	biimpri	Could not format ( _om ~<_ ( _J0 ` <. A , B >. ) -> -. ( _J0 ` <. A , B >. ) e. Fin ) : No typesetting found for |- ( _om ~<_ ( _J0 ` <. A , B >. ) -> -. ( _J0 ` <. A , B >. ) e. Fin ) with typecode |-
31	26 30	nsyli	Could not format ( ( A e. On /\ B e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> -. suc ( A u. B ) e. Fin ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> -. suc ( A u. B ) e. Fin ) ) with typecode |-
32		onun2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A\cup B\in \mathrm{On}$$
33		onsuc	$$⊢A\cup B\in \mathrm{On}\to \mathrm{suc}\left(A\cup B\right)\in \mathrm{On}$$
34		onenon	$$⊢\mathrm{suc}\left(A\cup B\right)\in \mathrm{On}\to \mathrm{suc}\left(A\cup B\right)\in \mathrm{dom}\mathrm{card}$$
35	32 33 34	3syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \mathrm{suc}\left(A\cup B\right)\in \mathrm{dom}\mathrm{card}$$
36		infinfnum	$$⊢\mathrm{suc}\left(A\cup B\right)\in \mathrm{dom}\mathrm{card}\to \left(\neg \mathrm{suc}\left(A\cup B\right)\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\preccurlyeq \mathrm{suc}\left(A\cup B\right)\right)$$
37	35 36	syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\neg \mathrm{suc}\left(A\cup B\right)\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\preccurlyeq \mathrm{suc}\left(A\cup B\right)\right)$$
38	31 37	sylibd	Could not format ( ( A e. On /\ B e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ suc ( A u. B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ suc ( A u. B ) ) ) with typecode |-
39	19 38	syl	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ suc ( A u. B ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ suc ( A u. B ) ) ) with typecode |-
40		infxpidm2	$$⊢\left(\mathrm{suc}\left(A\cup B\right)\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq \mathrm{suc}\left(A\cup B\right)\right)\to \left(\mathrm{suc}\left(A\cup B\right)\times \mathrm{suc}\left(A\cup B\right)\right)\approx \mathrm{suc}\left(A\cup B\right)$$
41	35 40	sylan	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \mathrm{\omega }\preccurlyeq \mathrm{suc}\left(A\cup B\right)\right)\to \left(\mathrm{suc}\left(A\cup B\right)\times \mathrm{suc}\left(A\cup B\right)\right)\approx \mathrm{suc}\left(A\cup B\right)$$
42	41	ex	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\mathrm{\omega }\preccurlyeq \mathrm{suc}\left(A\cup B\right)\to \left(\mathrm{suc}\left(A\cup B\right)\times \mathrm{suc}\left(A\cup B\right)\right)\approx \mathrm{suc}\left(A\cup B\right)\right)$$
43		domentr	Could not format ( ( ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) /\ ( suc ( A u. B ) X. suc ( A u. B ) ) ~~ suc ( A u. B ) ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) ) : No typesetting found for |- ( ( ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) /\ ( suc ( A u. B ) X. suc ( A u. B ) ) ~~ suc ( A u. B ) ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) ) with typecode |-
44	20 42 43	syl6an	Could not format ( ( A e. On /\ B e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) ) ) with typecode |-
45	19 44	syl	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) ) ) with typecode |-
46		onunel	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge \aleph \left(C\right)\in \mathrm{On}\right)\to \left(A\cup B\in \aleph \left(C\right)\leftrightarrow \left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\right)\right)$$
47	15 46	mp3an3	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\cup B\in \aleph \left(C\right)\leftrightarrow \left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\right)\right)$$
48	16 17 47	syl2an	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\right)\to \left(A\cup B\in \aleph \left(C\right)\leftrightarrow \left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\right)\right)$$
49	48	ibir	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\right)\to A\cup B\in \aleph \left(C\right)$$
50	49	3adant3	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\wedge C\in \mathrm{On}\right)\to A\cup B\in \aleph \left(C\right)$$
51		alephislim	$$⊢C\in \mathrm{On}\leftrightarrow \mathrm{Lim}\aleph \left(C\right)$$
52		limsuc	$$⊢\mathrm{Lim}\aleph \left(C\right)\to \left(A\cup B\in \aleph \left(C\right)\leftrightarrow \mathrm{suc}\left(A\cup B\right)\in \aleph \left(C\right)\right)$$
53	51 52	sylbi	$$⊢C\in \mathrm{On}\to \left(A\cup B\in \aleph \left(C\right)\leftrightarrow \mathrm{suc}\left(A\cup B\right)\in \aleph \left(C\right)\right)$$
54	53	3ad2ant3	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\wedge C\in \mathrm{On}\right)\to \left(A\cup B\in \aleph \left(C\right)\leftrightarrow \mathrm{suc}\left(A\cup B\right)\in \aleph \left(C\right)\right)$$
55	50 54	mpbid	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\wedge C\in \mathrm{On}\right)\to \mathrm{suc}\left(A\cup B\right)\in \aleph \left(C\right)$$
56	18 32 33	3syl	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\right)\to \mathrm{suc}\left(A\cup B\right)\in \mathrm{On}$$
57		alephsdom	$$⊢\left(\mathrm{suc}\left(A\cup B\right)\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to \left(\mathrm{suc}\left(A\cup B\right)\in \aleph \left(C\right)\leftrightarrow \mathrm{suc}\left(A\cup B\right)\prec \aleph \left(C\right)\right)$$
58	56 57	stoic3	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\wedge C\in \mathrm{On}\right)\to \left(\mathrm{suc}\left(A\cup B\right)\in \aleph \left(C\right)\leftrightarrow \mathrm{suc}\left(A\cup B\right)\prec \aleph \left(C\right)\right)$$
59	55 58	mpbid	$$⊢\left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\wedge C\in \mathrm{On}\right)\to \mathrm{suc}\left(A\cup B\right)\prec \aleph \left(C\right)$$
60	45 59	jctird	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) /\ suc ( A u. B ) ~< ( aleph ` C ) ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) /\ suc ( A u. B ) ~< ( aleph ` C ) ) ) ) with typecode |-
61		domsdomtr	Could not format ( ( ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) /\ suc ( A u. B ) ~< ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) : No typesetting found for |- ( ( ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) /\ suc ( A u. B ) ~< ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) with typecode |-
62	60 61	syl6	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) with typecode |-
63	39 62	syld	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) with typecode |-
64		alephsdom	Could not format ( ( ( _J0 ` <. A , B >. ) e. On /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) : No typesetting found for |- ( ( ( _J0 ` <. A , B >. ) e. On /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) with typecode |-
65	7 64	mpan	Could not format ( C e. On -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) : No typesetting found for |- ( C e. On -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) with typecode |-
66	65	3ad2ant3	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) ) with typecode |-
67	63 66	sylibrd	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) with typecode |-
68		alephgeom	$$⊢C\in \mathrm{On}\leftrightarrow \mathrm{\omega }\subseteq \aleph \left(C\right)$$
69	68	biimpi	$$⊢C\in \mathrm{On}\to \mathrm{\omega }\subseteq \aleph \left(C\right)$$
70	69	sselda	Could not format ( ( C e. On /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) : No typesetting found for |- ( ( C e. On /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) with typecode |-
71	70	3ad2antl3	Could not format ( ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) with typecode |-
72	71	ex	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. _om -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. _om -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) with typecode |-
73	67 72	jaod	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _om ~<_ ( _J0 ` <. A , B >. ) \/ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _om ~<_ ( _J0 ` <. A , B >. ) \/ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) with typecode |-
74	14 73	mpi	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) with typecode |-
75	74	3expia	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( C e. On -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( C e. On -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) with typecode |-
76	75	com12	Could not format ( C e. On -> ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) : No typesetting found for |- ( C e. On -> ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) with typecode |-
77		alephfnon	$$⊢\aleph Fn\mathrm{On}$$
78	77	fndmi	$$⊢\mathrm{dom}\aleph =\mathrm{On}$$
79	78	eleq2i	$$⊢C\in \mathrm{dom}\aleph \leftrightarrow C\in \mathrm{On}$$
80		ndmfv	$$⊢\neg C\in \mathrm{dom}\aleph \to \aleph \left(C\right)=\varnothing$$
81	79 80	sylnbir	$$⊢\neg C\in \mathrm{On}\to \aleph \left(C\right)=\varnothing$$
82		nel02	$$⊢\aleph \left(C\right)=\varnothing \to \neg A\in \aleph \left(C\right)$$
83	81 82	syl	$$⊢\neg C\in \mathrm{On}\to \neg A\in \aleph \left(C\right)$$
84	83	intnanrd	$$⊢\neg C\in \mathrm{On}\to \neg \left(A\in \aleph \left(C\right)\wedge B\in \aleph \left(C\right)\right)$$
85	84	pm2.21d	Could not format ( -. C e. On -> ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) : No typesetting found for |- ( -. C e. On -> ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) ) with typecode |-
86	76 85	pm2.61i	Could not format ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) : No typesetting found for |- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) with typecode |-