Theorem maxssj0

Description: The value of _J0 is at least the maximum of its two arguments. Proposition 15.1(1) of TakeutiZaring p. 154. (Contributed by BTernaryTau, 22-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		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 |-
2		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 |-
3		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 |-
4	1 2 3	mp2b	Could not format _J0 : ( On X. On ) --> On : No typesetting found for |- _J0 : ( On X. On ) --> On with typecode |-
5		0elon	$$⊢\varnothing \in \mathrm{On}$$
6	4 5	f0cli	Could not format ( _J0 ` <. A , B >. ) e. On : No typesetting found for |- ( _J0 ` <. A , B >. ) e. On with typecode |-
7	5	a1i	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \varnothing \in \mathrm{On}$$
8		onun2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A\cup B\in \mathrm{On}$$
9	7 8	opelxpd	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to ⟨\varnothing ,A\cup B⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
10		opelxpi	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to ⟨A,B⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
11		isorel	Could not format ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ ( <. (/) , ( A u. B ) >. e. ( On X. On ) /\ <. A , B >. e. ( On X. On ) ) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ ( <. (/) , ( A u. B ) >. e. ( On X. On ) /\ <. A , B >. e. ( On X. On ) ) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) ) with typecode |-
12	1 11	mpan	Could not format ( ( <. (/) , ( A u. B ) >. e. ( On X. On ) /\ <. A , B >. e. ( On X. On ) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( <. (/) , ( A u. B ) >. e. ( On X. On ) /\ <. A , B >. e. ( On X. On ) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) ) with typecode |-
13	9 10 12	syl2anc	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) ) with typecode |-
14		fvex	Could not format ( _J0 ` <. A , B >. ) e. _V : No typesetting found for |- ( _J0 ` <. A , B >. ) e. _V with typecode |-
15	14	epeli	Could not format ( ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) <-> ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) <-> ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) with typecode |-
16	13 15	bitrdi	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) ) with typecode |-
17		fvex	Could not format ( _J0 ` <. (/) , x >. ) e. _V : No typesetting found for |- ( _J0 ` <. (/) , x >. ) e. _V with typecode |-
18		eqid	Could not format ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) = ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) : No typesetting found for |- ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) = ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) with typecode |-
19	17 18	fnmpti	Could not format ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) Fn On : No typesetting found for |- ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) Fn On with typecode |-
20	18	j00smo	Could not format Smo ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) : No typesetting found for |- Smo ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) with typecode |-
21		smogt	Could not format ( ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) Fn On /\ Smo ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) /\ ( A u. B ) e. On ) -> ( A u. B ) C_ ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) ) : No typesetting found for |- ( ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) Fn On /\ Smo ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) /\ ( A u. B ) e. On ) -> ( A u. B ) C_ ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) ) with typecode |-
22	19 20 21	mp3an12	Could not format ( ( A u. B ) e. On -> ( A u. B ) C_ ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) ) : No typesetting found for |- ( ( A u. B ) e. On -> ( A u. B ) C_ ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) ) with typecode |-
23		opeq2	$$⊢x=A\cup B\to ⟨\varnothing ,x⟩=⟨\varnothing ,A\cup B⟩$$
24	23	fveq2d	Could not format ( x = ( A u. B ) -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , ( A u. B ) >. ) ) : No typesetting found for |- ( x = ( A u. B ) -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , ( A u. B ) >. ) ) with typecode |-
25		fvex	Could not format ( _J0 ` <. (/) , ( A u. B ) >. ) e. _V : No typesetting found for |- ( _J0 ` <. (/) , ( A u. B ) >. ) e. _V with typecode |-
26	24 18 25	fvmpt	Could not format ( ( A u. B ) e. On -> ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) = ( _J0 ` <. (/) , ( A u. B ) >. ) ) : No typesetting found for |- ( ( A u. B ) e. On -> ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) = ( _J0 ` <. (/) , ( A u. B ) >. ) ) with typecode |-
27	22 26	sseqtrd	Could not format ( ( A u. B ) e. On -> ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) ) : No typesetting found for |- ( ( A u. B ) e. On -> ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) ) with typecode |-
28	8 27	syl	Could not format ( ( A e. On /\ B e. On ) -> ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) ) with typecode |-
29		ontr2	Could not format ( ( ( A u. B ) e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) /\ ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( ( A u. B ) e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) /\ ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) ) with typecode |-
30	8 6 29	sylancl	Could not format ( ( A e. On /\ B e. On ) -> ( ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) /\ ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) /\ ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) ) with typecode |-
31	28 30	mpand	Could not format ( ( A e. On /\ B e. On ) -> ( ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) ) with typecode |-
32	16 31	sylbid	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) ) with typecode |-
33		onelss	Could not format ( ( _J0 ` <. A , B >. ) e. On -> ( ( A u. B ) e. ( _J0 ` <. A , B >. ) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. On -> ( ( A u. B ) e. ( _J0 ` <. A , B >. ) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) ) with typecode |-
34	6 32 33	mpsylsyld	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) ) with typecode |-
35		eqcom	$$⊢A=\varnothing \leftrightarrow \varnothing =A$$
36	35	biimpi	$$⊢A=\varnothing \to \varnothing =A$$
37		uneq1	$$⊢A=\varnothing \to A\cup B=\varnothing \cup B$$
38		0un	$$⊢\varnothing \cup B=B$$
39	37 38	eqtrdi	$$⊢A=\varnothing \to A\cup B=B$$
40	36 39	opeq12d	$$⊢A=\varnothing \to ⟨\varnothing ,A\cup B⟩=⟨A,B⟩$$
41	40	fveq2d	Could not format ( A = (/) -> ( _J0 ` <. (/) , ( A u. B ) >. ) = ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( A = (/) -> ( _J0 ` <. (/) , ( A u. B ) >. ) = ( _J0 ` <. A , B >. ) ) with typecode |-
42	41	sseq2d	Could not format ( A = (/) -> ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) <-> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( A = (/) -> ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) <-> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) ) with typecode |-
43	28 42	syl5ibcom	Could not format ( ( A e. On /\ B e. On ) -> ( A = (/) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A = (/) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) ) with typecode |-
44		0un	$$⊢\varnothing \cup \left(A\cup B\right)=A\cup B$$
45	44	a1i	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \varnothing \cup \left(A\cup B\right)=A\cup B$$
46		simpl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A\in \mathrm{On}$$
47		simpr	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to B\in \mathrm{On}$$
48	7 8 46 47	brr0d	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) ) with typecode |-
49		eloni	$$⊢A\cup B\in \mathrm{On}\to \mathrm{Ord}\left(A\cup B\right)$$
50		ordirr	$$⊢\mathrm{Ord}\left(A\cup B\right)\to \neg A\cup B\in \left(A\cup B\right)$$
51	8 49 50	3syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \neg A\cup B\in \left(A\cup B\right)$$
52	44	eleq1i	$$⊢\varnothing \cup \left(A\cup B\right)\in \left(A\cup B\right)\leftrightarrow A\cup B\in \left(A\cup B\right)$$
53	51 52	sylnibr	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \neg \varnothing \cup \left(A\cup B\right)\in \left(A\cup B\right)$$
54		orel1	Could not format ( -. ( (/) u. ( A u. B ) ) e. ( A u. B ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) -> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) : No typesetting found for |- ( -. ( (/) u. ( A u. B ) ) e. ( A u. B ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) -> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) with typecode |-
55		olc	Could not format ( ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) -> ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) : No typesetting found for |- ( ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) -> ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) with typecode |-
56	54 55	impbid1	Could not format ( -. ( (/) u. ( A u. B ) ) e. ( A u. B ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) : No typesetting found for |- ( -. ( (/) u. ( A u. B ) ) e. ( A u. B ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) with typecode |-
57	53 56	syl	Could not format ( ( A e. On /\ B e. On ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) with typecode |-
58	48 57	bitrd	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) with typecode |-
59	45 58	mpbirand	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) with typecode |-
60	7 8 46 47	brlexod	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. LexOrd <. A , B >. <-> ( (/) e. A \/ ( (/) = A /\ ( A u. B ) e. B ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. LexOrd <. A , B >. <-> ( (/) e. A \/ ( (/) = A /\ ( A u. B ) e. B ) ) ) ) with typecode |-
61		eloni	$$⊢B\in \mathrm{On}\to \mathrm{Ord}B$$
62		ordirr	$$⊢\mathrm{Ord}B\to \neg B\in B$$
63	61 62	syl	$$⊢B\in \mathrm{On}\to \neg B\in B$$
64	63	intnand	$$⊢B\in \mathrm{On}\to \neg \left(A\in B\wedge B\in B\right)$$
65	64	adantl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \neg \left(A\in B\wedge B\in B\right)$$
66		onunel	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\cup B\in B\leftrightarrow \left(A\in B\wedge B\in B\right)\right)$$
67	66	3anidm23	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\cup B\in B\leftrightarrow \left(A\in B\wedge B\in B\right)\right)$$
68	65 67	mtbird	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \neg A\cup B\in B$$
69	68	intnand	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \neg \left(\varnothing =A\wedge A\cup B\in B\right)$$
70		orel2	$$⊢\neg \left(\varnothing =A\wedge A\cup B\in B\right)\to \left(\left(\varnothing \in A\vee \left(\varnothing =A\wedge A\cup B\in B\right)\right)\to \varnothing \in A\right)$$
71		orc	$$⊢\varnothing \in A\to \left(\varnothing \in A\vee \left(\varnothing =A\wedge A\cup B\in B\right)\right)$$
72	70 71	impbid1	$$⊢\neg \left(\varnothing =A\wedge A\cup B\in B\right)\to \left(\left(\varnothing \in A\vee \left(\varnothing =A\wedge A\cup B\in B\right)\right)\leftrightarrow \varnothing \in A\right)$$
73	69 72	syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\left(\varnothing \in A\vee \left(\varnothing =A\wedge A\cup B\in B\right)\right)\leftrightarrow \varnothing \in A\right)$$
74	59 60 73	3bitrd	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> (/) e. A ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> (/) e. A ) ) with typecode |-
75		on0eln0	$$⊢A\in \mathrm{On}\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$
76	75	adantr	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$
77		df-ne	$$⊢A\ne \varnothing \leftrightarrow \neg A=\varnothing$$
78	76 77	bitrdi	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\varnothing \in A\leftrightarrow \neg A=\varnothing \right)$$
79	74 78	bitrd	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) ) with typecode |-
80		xor3	Could not format ( -. ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> A = (/) ) <-> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) ) : No typesetting found for |- ( -. ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> A = (/) ) <-> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) ) with typecode |-
81		nbior	Could not format ( -. ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> A = (/) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) ) : No typesetting found for |- ( -. ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> A = (/) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) ) with typecode |-
82	80 81	sylbir	Could not format ( ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) ) : No typesetting found for |- ( ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) ) with typecode |-
83	79 82	syl	Could not format ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) ) with typecode |-
84	34 43 83	mpjaod	Could not format ( ( A e. On /\ B e. On ) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) with typecode |-