Theorem naddunif

Description: Uniformity theorem for natural addition. If A is the upper bound of X and B is the upper bound of Y , then ( A +no B ) can be expressed in terms of X and Y . (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Hypotheses	naddunif.1	$$⊢\phi \to A\in \mathrm{On}$$
	naddunif.2	$$⊢\phi \to B\in \mathrm{On}$$
	naddunif.3	$$⊢\phi \to A=\bigcap \left\{x\in \mathrm{On}|X\subseteq x\right\}$$
	naddunif.4	$$⊢\phi \to B=\bigcap \left\{y\in \mathrm{On}|Y\subseteq y\right\}$$
Assertion	naddunif	Could not format assertion : No typesetting found for |- ( ph -> ( A +no B ) = |^| { z e. On | ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) C_ z } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		naddunif.1	$$⊢\phi \to A\in \mathrm{On}$$
2		naddunif.2	$$⊢\phi \to B\in \mathrm{On}$$
3		naddunif.3	$$⊢\phi \to A=\bigcap \left\{x\in \mathrm{On}|X\subseteq x\right\}$$
4		naddunif.4	$$⊢\phi \to B=\bigcap \left\{y\in \mathrm{On}|Y\subseteq y\right\}$$
5		naddov3	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } ) with typecode |-
6	1 2 5	syl2anc	Could not format ( ph -> ( A +no B ) = |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } ) : No typesetting found for |- ( ph -> ( A +no B ) = |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } ) with typecode |-
7		naddfn	Could not format +no Fn ( On X. On ) : No typesetting found for |- +no Fn ( On X. On ) with typecode |-
8		fnfun	Could not format ( +no Fn ( On X. On ) -> Fun +no ) : No typesetting found for |- ( +no Fn ( On X. On ) -> Fun +no ) with typecode |-
9	7 8	ax-mp	Could not format Fun +no : No typesetting found for |- Fun +no with typecode |-
10		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
11		xpexg	$$⊢\left(\left\{A\right\}\in \mathrm{V}\wedge B\in \mathrm{On}\right)\to \left\{A\right\}\times B\in \mathrm{V}$$
12	10 2 11	sylancr	$$⊢\phi \to \left\{A\right\}\times B\in \mathrm{V}$$
13		funimaexg	Could not format ( ( Fun +no /\ ( { A } X. B ) e. _V ) -> ( +no " ( { A } X. B ) ) e. _V ) : No typesetting found for |- ( ( Fun +no /\ ( { A } X. B ) e. _V ) -> ( +no " ( { A } X. B ) ) e. _V ) with typecode |-
14	9 12 13	sylancr	Could not format ( ph -> ( +no " ( { A } X. B ) ) e. _V ) : No typesetting found for |- ( ph -> ( +no " ( { A } X. B ) ) e. _V ) with typecode |-
15		imassrn	Could not format ( +no " ( { A } X. B ) ) C_ ran +no : No typesetting found for |- ( +no " ( { A } X. B ) ) C_ ran +no with typecode |-
16		naddf	Could not format +no : ( On X. On ) --> On : No typesetting found for |- +no : ( On X. On ) --> On with typecode |-
17		frn	Could not format ( +no : ( On X. On ) --> On -> ran +no C_ On ) : No typesetting found for |- ( +no : ( On X. On ) --> On -> ran +no C_ On ) with typecode |-
18	16 17	ax-mp	Could not format ran +no C_ On : No typesetting found for |- ran +no C_ On with typecode |-
19	15 18	sstri	Could not format ( +no " ( { A } X. B ) ) C_ On : No typesetting found for |- ( +no " ( { A } X. B ) ) C_ On with typecode |-
20	19	a1i	Could not format ( ph -> ( +no " ( { A } X. B ) ) C_ On ) : No typesetting found for |- ( ph -> ( +no " ( { A } X. B ) ) C_ On ) with typecode |-
21	14 20	elpwd	Could not format ( ph -> ( +no " ( { A } X. B ) ) e. ~P On ) : No typesetting found for |- ( ph -> ( +no " ( { A } X. B ) ) e. ~P On ) with typecode |-
22		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
23		xpexg	$$⊢\left(A\in \mathrm{On}\wedge \left\{B\right\}\in \mathrm{V}\right)\to A\times \left\{B\right\}\in \mathrm{V}$$
24	1 22 23	sylancl	$$⊢\phi \to A\times \left\{B\right\}\in \mathrm{V}$$
25		funimaexg	Could not format ( ( Fun +no /\ ( A X. { B } ) e. _V ) -> ( +no " ( A X. { B } ) ) e. _V ) : No typesetting found for |- ( ( Fun +no /\ ( A X. { B } ) e. _V ) -> ( +no " ( A X. { B } ) ) e. _V ) with typecode |-
26	9 24 25	sylancr	Could not format ( ph -> ( +no " ( A X. { B } ) ) e. _V ) : No typesetting found for |- ( ph -> ( +no " ( A X. { B } ) ) e. _V ) with typecode |-
27		imassrn	Could not format ( +no " ( A X. { B } ) ) C_ ran +no : No typesetting found for |- ( +no " ( A X. { B } ) ) C_ ran +no with typecode |-
28	27 18	sstri	Could not format ( +no " ( A X. { B } ) ) C_ On : No typesetting found for |- ( +no " ( A X. { B } ) ) C_ On with typecode |-
29	28	a1i	Could not format ( ph -> ( +no " ( A X. { B } ) ) C_ On ) : No typesetting found for |- ( ph -> ( +no " ( A X. { B } ) ) C_ On ) with typecode |-
30	26 29	elpwd	Could not format ( ph -> ( +no " ( A X. { B } ) ) e. ~P On ) : No typesetting found for |- ( ph -> ( +no " ( A X. { B } ) ) e. ~P On ) with typecode |-
31		pwuncl	Could not format ( ( ( +no " ( { A } X. B ) ) e. ~P On /\ ( +no " ( A X. { B } ) ) e. ~P On ) -> ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) e. ~P On ) : No typesetting found for |- ( ( ( +no " ( { A } X. B ) ) e. ~P On /\ ( +no " ( A X. { B } ) ) e. ~P On ) -> ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) e. ~P On ) with typecode |-
32	21 30 31	syl2anc	Could not format ( ph -> ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) e. ~P On ) : No typesetting found for |- ( ph -> ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) e. ~P On ) with typecode |-
33	3 1	eqeltrrd	$$⊢\phi \to \bigcap \left\{x\in \mathrm{On}|X\subseteq x\right\}\in \mathrm{On}$$
34		onintrab2	$$⊢\exists x\in \mathrm{On}X\subseteq x\leftrightarrow \bigcap \left\{x\in \mathrm{On}|X\subseteq x\right\}\in \mathrm{On}$$
35	33 34	sylibr	$$⊢\phi \to \exists x\in \mathrm{On}X\subseteq x$$
36		vex	$$⊢x\in \mathrm{V}$$
37	36	ssex	$$⊢X\subseteq x\to X\in \mathrm{V}$$
38	37	rexlimivw	$$⊢\exists x\in \mathrm{On}X\subseteq x\to X\in \mathrm{V}$$
39	35 38	syl	$$⊢\phi \to X\in \mathrm{V}$$
40		xpexg	$$⊢\left(X\in \mathrm{V}\wedge \left\{B\right\}\in \mathrm{V}\right)\to X\times \left\{B\right\}\in \mathrm{V}$$
41	39 22 40	sylancl	$$⊢\phi \to X\times \left\{B\right\}\in \mathrm{V}$$
42		funimaexg	Could not format ( ( Fun +no /\ ( X X. { B } ) e. _V ) -> ( +no " ( X X. { B } ) ) e. _V ) : No typesetting found for |- ( ( Fun +no /\ ( X X. { B } ) e. _V ) -> ( +no " ( X X. { B } ) ) e. _V ) with typecode |-
43	9 41 42	sylancr	Could not format ( ph -> ( +no " ( X X. { B } ) ) e. _V ) : No typesetting found for |- ( ph -> ( +no " ( X X. { B } ) ) e. _V ) with typecode |-
44		imassrn	Could not format ( +no " ( X X. { B } ) ) C_ ran +no : No typesetting found for |- ( +no " ( X X. { B } ) ) C_ ran +no with typecode |-
45	44 18	sstri	Could not format ( +no " ( X X. { B } ) ) C_ On : No typesetting found for |- ( +no " ( X X. { B } ) ) C_ On with typecode |-
46	45	a1i	Could not format ( ph -> ( +no " ( X X. { B } ) ) C_ On ) : No typesetting found for |- ( ph -> ( +no " ( X X. { B } ) ) C_ On ) with typecode |-
47	43 46	elpwd	Could not format ( ph -> ( +no " ( X X. { B } ) ) e. ~P On ) : No typesetting found for |- ( ph -> ( +no " ( X X. { B } ) ) e. ~P On ) with typecode |-
48	4 2	eqeltrrd	$$⊢\phi \to \bigcap \left\{y\in \mathrm{On}|Y\subseteq y\right\}\in \mathrm{On}$$
49		onintrab2	$$⊢\exists y\in \mathrm{On}Y\subseteq y\leftrightarrow \bigcap \left\{y\in \mathrm{On}|Y\subseteq y\right\}\in \mathrm{On}$$
50	48 49	sylibr	$$⊢\phi \to \exists y\in \mathrm{On}Y\subseteq y$$
51		vex	$$⊢y\in \mathrm{V}$$
52	51	ssex	$$⊢Y\subseteq y\to Y\in \mathrm{V}$$
53	52	rexlimivw	$$⊢\exists y\in \mathrm{On}Y\subseteq y\to Y\in \mathrm{V}$$
54	50 53	syl	$$⊢\phi \to Y\in \mathrm{V}$$
55		xpexg	$$⊢\left(\left\{A\right\}\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to \left\{A\right\}\times Y\in \mathrm{V}$$
56	10 54 55	sylancr	$$⊢\phi \to \left\{A\right\}\times Y\in \mathrm{V}$$
57		funimaexg	Could not format ( ( Fun +no /\ ( { A } X. Y ) e. _V ) -> ( +no " ( { A } X. Y ) ) e. _V ) : No typesetting found for |- ( ( Fun +no /\ ( { A } X. Y ) e. _V ) -> ( +no " ( { A } X. Y ) ) e. _V ) with typecode |-
58	9 56 57	sylancr	Could not format ( ph -> ( +no " ( { A } X. Y ) ) e. _V ) : No typesetting found for |- ( ph -> ( +no " ( { A } X. Y ) ) e. _V ) with typecode |-
59		imassrn	Could not format ( +no " ( { A } X. Y ) ) C_ ran +no : No typesetting found for |- ( +no " ( { A } X. Y ) ) C_ ran +no with typecode |-
60	59 18	sstri	Could not format ( +no " ( { A } X. Y ) ) C_ On : No typesetting found for |- ( +no " ( { A } X. Y ) ) C_ On with typecode |-
61	60	a1i	Could not format ( ph -> ( +no " ( { A } X. Y ) ) C_ On ) : No typesetting found for |- ( ph -> ( +no " ( { A } X. Y ) ) C_ On ) with typecode |-
62	58 61	elpwd	Could not format ( ph -> ( +no " ( { A } X. Y ) ) e. ~P On ) : No typesetting found for |- ( ph -> ( +no " ( { A } X. Y ) ) e. ~P On ) with typecode |-
63		pwuncl	Could not format ( ( ( +no " ( X X. { B } ) ) e. ~P On /\ ( +no " ( { A } X. Y ) ) e. ~P On ) -> ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) e. ~P On ) : No typesetting found for |- ( ( ( +no " ( X X. { B } ) ) e. ~P On /\ ( +no " ( { A } X. Y ) ) e. ~P On ) -> ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) e. ~P On ) with typecode |-
64	47 62 63	syl2anc	Could not format ( ph -> ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) e. ~P On ) : No typesetting found for |- ( ph -> ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) e. ~P On ) with typecode |-
65	2 4	cofonr	$$⊢\phi \to \forall q\in B\exists s\in Yq\subseteq s$$
66		onss	$$⊢B\in \mathrm{On}\to B\subseteq \mathrm{On}$$
67	2 66	syl	$$⊢\phi \to B\subseteq \mathrm{On}$$
68	67	sselda	$$⊢\left(\phi \wedge q\in B\right)\to q\in \mathrm{On}$$
69	68	adantr	$$⊢\left(\left(\phi \wedge q\in B\right)\wedge s\in Y\right)\to q\in \mathrm{On}$$
70		onss	$$⊢y\in \mathrm{On}\to y\subseteq \mathrm{On}$$
71	70	adantl	$$⊢\left(\phi \wedge y\in \mathrm{On}\right)\to y\subseteq \mathrm{On}$$
72		sstr	$$⊢\left(Y\subseteq y\wedge y\subseteq \mathrm{On}\right)\to Y\subseteq \mathrm{On}$$
73	72	expcom	$$⊢y\subseteq \mathrm{On}\to \left(Y\subseteq y\to Y\subseteq \mathrm{On}\right)$$
74	71 73	syl	$$⊢\left(\phi \wedge y\in \mathrm{On}\right)\to \left(Y\subseteq y\to Y\subseteq \mathrm{On}\right)$$
75	74	rexlimdva	$$⊢\phi \to \left(\exists y\in \mathrm{On}Y\subseteq y\to Y\subseteq \mathrm{On}\right)$$
76	50 75	mpd	$$⊢\phi \to Y\subseteq \mathrm{On}$$
77	76	adantr	$$⊢\left(\phi \wedge q\in B\right)\to Y\subseteq \mathrm{On}$$
78	77	sselda	$$⊢\left(\left(\phi \wedge q\in B\right)\wedge s\in Y\right)\to s\in \mathrm{On}$$
79	1	ad2antrr	$$⊢\left(\left(\phi \wedge q\in B\right)\wedge s\in Y\right)\to A\in \mathrm{On}$$
80		naddss2	Could not format ( ( q e. On /\ s e. On /\ A e. On ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ( q e. On /\ s e. On /\ A e. On ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
81	69 78 79 80	syl3anc	Could not format ( ( ( ph /\ q e. B ) /\ s e. Y ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ( ( ph /\ q e. B ) /\ s e. Y ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
82	81	rexbidva	Could not format ( ( ph /\ q e. B ) -> ( E. s e. Y q C_ s <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ( ph /\ q e. B ) -> ( E. s e. Y q C_ s <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
83	82	ralbidva	Could not format ( ph -> ( A. q e. B E. s e. Y q C_ s <-> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ph -> ( A. q e. B E. s e. Y q C_ s <-> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
84	65 83	mpbid	Could not format ( ph -> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) ) : No typesetting found for |- ( ph -> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) ) with typecode |-
85	1	snssd	$$⊢\phi \to \left\{A\right\}\subseteq \mathrm{On}$$
86		xpss12	$$⊢\left(\left\{A\right\}\subseteq \mathrm{On}\wedge Y\subseteq \mathrm{On}\right)\to \left\{A\right\}\times Y\subseteq \mathrm{On}\times \mathrm{On}$$
87	85 76 86	syl2anc	$$⊢\phi \to \left\{A\right\}\times Y\subseteq \mathrm{On}\times \mathrm{On}$$
88		sseq2	Could not format ( d = ( r +no s ) -> ( ( A +no q ) C_ d <-> ( A +no q ) C_ ( r +no s ) ) ) : No typesetting found for |- ( d = ( r +no s ) -> ( ( A +no q ) C_ d <-> ( A +no q ) C_ ( r +no s ) ) ) with typecode |-
89	88	imaeqexov	Could not format ( ( +no Fn ( On X. On ) /\ ( { A } X. Y ) C_ ( On X. On ) ) -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( { A } X. Y ) C_ ( On X. On ) ) -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) ) ) with typecode |-
90	7 87 89	sylancr	Could not format ( ph -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ph -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) ) ) with typecode |-
91		oveq1	Could not format ( r = A -> ( r +no s ) = ( A +no s ) ) : No typesetting found for |- ( r = A -> ( r +no s ) = ( A +no s ) ) with typecode |-
92	91	sseq2d	Could not format ( r = A -> ( ( A +no q ) C_ ( r +no s ) <-> ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( r = A -> ( ( A +no q ) C_ ( r +no s ) <-> ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
93	92	rexbidv	Could not format ( r = A -> ( E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( r = A -> ( E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
94	93	rexsng	Could not format ( A e. On -> ( E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( A e. On -> ( E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
95	1 94	syl	Could not format ( ph -> ( E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ph -> ( E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
96	90 95	bitrd	Could not format ( ph -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ph -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
97	96	ralbidv	Could not format ( ph -> ( A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ph -> ( A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
98	84 97	mpbird	Could not format ( ph -> A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) : No typesetting found for |- ( ph -> A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) with typecode |-
99		olc	Could not format ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d -> ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d -> ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) with typecode |-
100	99	ralimi	Could not format ( A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d -> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d -> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) with typecode |-
101	98 100	syl	Could not format ( ph -> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( ph -> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) with typecode |-
102		rexun	Could not format ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d <-> ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d <-> ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) with typecode |-
103	102	ralbii	Could not format ( A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d <-> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d <-> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) ) with typecode |-
104	101 103	sylibr	Could not format ( ph -> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) : No typesetting found for |- ( ph -> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) with typecode |-
105		xpss12	$$⊢\left(\left\{A\right\}\subseteq \mathrm{On}\wedge B\subseteq \mathrm{On}\right)\to \left\{A\right\}\times B\subseteq \mathrm{On}\times \mathrm{On}$$
106	85 67 105	syl2anc	$$⊢\phi \to \left\{A\right\}\times B\subseteq \mathrm{On}\times \mathrm{On}$$
107		sseq1	Could not format ( c = ( p +no q ) -> ( c C_ d <-> ( p +no q ) C_ d ) ) : No typesetting found for |- ( c = ( p +no q ) -> ( c C_ d <-> ( p +no q ) C_ d ) ) with typecode |-
108	107	rexbidv	Could not format ( c = ( p +no q ) -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) : No typesetting found for |- ( c = ( p +no q ) -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) with typecode |-
109	108	imaeqalov	Could not format ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) with typecode |-
110	7 106 109	sylancr	Could not format ( ph -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) : No typesetting found for |- ( ph -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) with typecode |-
111		oveq1	Could not format ( p = A -> ( p +no q ) = ( A +no q ) ) : No typesetting found for |- ( p = A -> ( p +no q ) = ( A +no q ) ) with typecode |-
112	111	sseq1d	Could not format ( p = A -> ( ( p +no q ) C_ d <-> ( A +no q ) C_ d ) ) : No typesetting found for |- ( p = A -> ( ( p +no q ) C_ d <-> ( A +no q ) C_ d ) ) with typecode |-
113	112	rexbidv	Could not format ( p = A -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( p = A -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) with typecode |-
114	113	ralbidv	Could not format ( p = A -> ( A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( p = A -> ( A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) with typecode |-
115	114	ralsng	Could not format ( A e. On -> ( A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( A e. On -> ( A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) with typecode |-
116	1 115	syl	Could not format ( ph -> ( A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( ph -> ( A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) with typecode |-
117	110 116	bitrd	Could not format ( ph -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) : No typesetting found for |- ( ph -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) ) with typecode |-
118	104 117	mpbird	Could not format ( ph -> A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) : No typesetting found for |- ( ph -> A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) with typecode |-
119	1 3	cofonr	$$⊢\phi \to \forall p\in A\exists r\in Xp\subseteq r$$
120		onss	$$⊢A\in \mathrm{On}\to A\subseteq \mathrm{On}$$
121	1 120	syl	$$⊢\phi \to A\subseteq \mathrm{On}$$
122	121	sselda	$$⊢\left(\phi \wedge p\in A\right)\to p\in \mathrm{On}$$
123	122	adantr	$$⊢\left(\left(\phi \wedge p\in A\right)\wedge r\in X\right)\to p\in \mathrm{On}$$
124		ssintub	$$⊢X\subseteq \bigcap \left\{x\in \mathrm{On}|X\subseteq x\right\}$$
125	3 121	eqsstrrd	$$⊢\phi \to \bigcap \left\{x\in \mathrm{On}|X\subseteq x\right\}\subseteq \mathrm{On}$$
126	124 125	sstrid	$$⊢\phi \to X\subseteq \mathrm{On}$$
127	126	adantr	$$⊢\left(\phi \wedge p\in A\right)\to X\subseteq \mathrm{On}$$
128	127	sselda	$$⊢\left(\left(\phi \wedge p\in A\right)\wedge r\in X\right)\to r\in \mathrm{On}$$
129	2	ad2antrr	$$⊢\left(\left(\phi \wedge p\in A\right)\wedge r\in X\right)\to B\in \mathrm{On}$$
130		naddss1	Could not format ( ( p e. On /\ r e. On /\ B e. On ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ( p e. On /\ r e. On /\ B e. On ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
131	123 128 129 130	syl3anc	Could not format ( ( ( ph /\ p e. A ) /\ r e. X ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ( ( ph /\ p e. A ) /\ r e. X ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
132	131	rexbidva	Could not format ( ( ph /\ p e. A ) -> ( E. r e. X p C_ r <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( E. r e. X p C_ r <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
133	132	ralbidva	Could not format ( ph -> ( A. p e. A E. r e. X p C_ r <-> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( A. p e. A E. r e. X p C_ r <-> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
134	119 133	mpbid	Could not format ( ph -> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) ) : No typesetting found for |- ( ph -> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) ) with typecode |-
135	2	snssd	$$⊢\phi \to \left\{B\right\}\subseteq \mathrm{On}$$
136		xpss12	$$⊢\left(X\subseteq \mathrm{On}\wedge \left\{B\right\}\subseteq \mathrm{On}\right)\to X\times \left\{B\right\}\subseteq \mathrm{On}\times \mathrm{On}$$
137	126 135 136	syl2anc	$$⊢\phi \to X\times \left\{B\right\}\subseteq \mathrm{On}\times \mathrm{On}$$
138		sseq2	Could not format ( d = ( r +no s ) -> ( ( p +no B ) C_ d <-> ( p +no B ) C_ ( r +no s ) ) ) : No typesetting found for |- ( d = ( r +no s ) -> ( ( p +no B ) C_ d <-> ( p +no B ) C_ ( r +no s ) ) ) with typecode |-
139	138	imaeqexov	Could not format ( ( +no Fn ( On X. On ) /\ ( X X. { B } ) C_ ( On X. On ) ) -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( X X. { B } ) C_ ( On X. On ) ) -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) ) ) with typecode |-
140	7 137 139	sylancr	Could not format ( ph -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ph -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) ) ) with typecode |-
141		oveq2	Could not format ( s = B -> ( r +no s ) = ( r +no B ) ) : No typesetting found for |- ( s = B -> ( r +no s ) = ( r +no B ) ) with typecode |-
142	141	sseq2d	Could not format ( s = B -> ( ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( s = B -> ( ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
143	142	rexsng	Could not format ( B e. On -> ( E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( B e. On -> ( E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
144	2 143	syl	Could not format ( ph -> ( E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
145	144	rexbidv	Could not format ( ph -> ( E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
146	140 145	bitrd	Could not format ( ph -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
147	146	ralbidv	Could not format ( ph -> ( A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
148	134 147	mpbird	Could not format ( ph -> A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d ) : No typesetting found for |- ( ph -> A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d ) with typecode |-
149		orc	Could not format ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) with typecode |-
150	149	ralimi	Could not format ( A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d -> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d -> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) with typecode |-
151	148 150	syl	Could not format ( ph -> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( ph -> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) with typecode |-
152		rexun	Could not format ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d <-> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d <-> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) with typecode |-
153	152	ralbii	Could not format ( A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d <-> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d <-> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) ) with typecode |-
154	151 153	sylibr	Could not format ( ph -> A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) : No typesetting found for |- ( ph -> A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) with typecode |-
155		oveq2	Could not format ( q = B -> ( p +no q ) = ( p +no B ) ) : No typesetting found for |- ( q = B -> ( p +no q ) = ( p +no B ) ) with typecode |-
156	155	sseq1d	Could not format ( q = B -> ( ( p +no q ) C_ d <-> ( p +no B ) C_ d ) ) : No typesetting found for |- ( q = B -> ( ( p +no q ) C_ d <-> ( p +no B ) C_ d ) ) with typecode |-
157	156	rexbidv	Could not format ( q = B -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( q = B -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) ) with typecode |-
158	157	ralsng	Could not format ( B e. On -> ( A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( B e. On -> ( A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) ) with typecode |-
159	2 158	syl	Could not format ( ph -> ( A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( ph -> ( A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) ) with typecode |-
160	159	ralbidv	Could not format ( ph -> ( A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) ) : No typesetting found for |- ( ph -> ( A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) ) with typecode |-
161	154 160	mpbird	Could not format ( ph -> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) : No typesetting found for |- ( ph -> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) with typecode |-
162		xpss12	$$⊢\left(A\subseteq \mathrm{On}\wedge \left\{B\right\}\subseteq \mathrm{On}\right)\to A\times \left\{B\right\}\subseteq \mathrm{On}\times \mathrm{On}$$
163	121 135 162	syl2anc	$$⊢\phi \to A\times \left\{B\right\}\subseteq \mathrm{On}\times \mathrm{On}$$
164	108	imaeqalov	Could not format ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) with typecode |-
165	7 163 164	sylancr	Could not format ( ph -> ( A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) : No typesetting found for |- ( ph -> ( A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) ) with typecode |-
166	161 165	mpbird	Could not format ( ph -> A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) : No typesetting found for |- ( ph -> A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) with typecode |-
167		ralunb	Could not format ( A. c e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d /\ A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) ) : No typesetting found for |- ( A. c e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d /\ A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) ) with typecode |-
168	118 166 167	sylanbrc	Could not format ( ph -> A. c e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) : No typesetting found for |- ( ph -> A. c e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) with typecode |-
169	124 3	sseqtrrid	$$⊢\phi \to X\subseteq A$$
170	169	sselda	$$⊢\left(\phi \wedge p\in X\right)\to p\in A$$
171		ssid	$$⊢p\subseteq p$$
172		sseq2	$$⊢r=p\to \left(p\subseteq r\leftrightarrow p\subseteq p\right)$$
173	172	rspcev	$$⊢\left(p\in A\wedge p\subseteq p\right)\to \exists r\in Ap\subseteq r$$
174	170 171 173	sylancl	$$⊢\left(\phi \wedge p\in X\right)\to \exists r\in Ap\subseteq r$$
175	174	ralrimiva	$$⊢\phi \to \forall p\in X\exists r\in Ap\subseteq r$$
176	126	sselda	$$⊢\left(\phi \wedge p\in X\right)\to p\in \mathrm{On}$$
177	176	adantr	$$⊢\left(\left(\phi \wedge p\in X\right)\wedge r\in A\right)\to p\in \mathrm{On}$$
178	121	adantr	$$⊢\left(\phi \wedge p\in X\right)\to A\subseteq \mathrm{On}$$
179	178	sselda	$$⊢\left(\left(\phi \wedge p\in X\right)\wedge r\in A\right)\to r\in \mathrm{On}$$
180	2	ad2antrr	$$⊢\left(\left(\phi \wedge p\in X\right)\wedge r\in A\right)\to B\in \mathrm{On}$$
181	177 179 180 130	syl3anc	Could not format ( ( ( ph /\ p e. X ) /\ r e. A ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ( ( ph /\ p e. X ) /\ r e. A ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
182	181	rexbidva	Could not format ( ( ph /\ p e. X ) -> ( E. r e. A p C_ r <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ( ph /\ p e. X ) -> ( E. r e. A p C_ r <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
183	182	ralbidva	Could not format ( ph -> ( A. p e. X E. r e. A p C_ r <-> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( A. p e. X E. r e. A p C_ r <-> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
184	175 183	mpbid	Could not format ( ph -> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) ) : No typesetting found for |- ( ph -> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) ) with typecode |-
185		sseq2	Could not format ( b = ( r +no s ) -> ( ( p +no B ) C_ b <-> ( p +no B ) C_ ( r +no s ) ) ) : No typesetting found for |- ( b = ( r +no s ) -> ( ( p +no B ) C_ b <-> ( p +no B ) C_ ( r +no s ) ) ) with typecode |-
186	185	imaeqexov	Could not format ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) ) ) with typecode |-
187	7 163 186	sylancr	Could not format ( ph -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ph -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) ) ) with typecode |-
188	144	rexbidv	Could not format ( ph -> ( E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
189	187 188	bitrd	Could not format ( ph -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
190	189	ralbidv	Could not format ( ph -> ( A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) ) ) : No typesetting found for |- ( ph -> ( A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) ) ) with typecode |-
191	184 190	mpbird	Could not format ( ph -> A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) : No typesetting found for |- ( ph -> A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) with typecode |-
192		olc	Could not format ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b -> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) : No typesetting found for |- ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b -> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) with typecode |-
193	192	ralimi	Could not format ( A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b -> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) : No typesetting found for |- ( A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b -> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) with typecode |-
194	191 193	syl	Could not format ( ph -> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) : No typesetting found for |- ( ph -> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) with typecode |-
195	155	sseq1d	Could not format ( q = B -> ( ( p +no q ) C_ b <-> ( p +no B ) C_ b ) ) : No typesetting found for |- ( q = B -> ( ( p +no q ) C_ b <-> ( p +no B ) C_ b ) ) with typecode |-
196	195	rexbidv	Could not format ( q = B -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) ) : No typesetting found for |- ( q = B -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) ) with typecode |-
197	196	ralsng	Could not format ( B e. On -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) ) : No typesetting found for |- ( B e. On -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) ) with typecode |-
198	2 197	syl	Could not format ( ph -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) ) : No typesetting found for |- ( ph -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) ) with typecode |-
199	198	adantr	Could not format ( ( ph /\ p e. X ) -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) ) : No typesetting found for |- ( ( ph /\ p e. X ) -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) ) with typecode |-
200		rexun	Could not format ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) : No typesetting found for |- ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) with typecode |-
201	199 200	bitrdi	Could not format ( ( ph /\ p e. X ) -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) ) : No typesetting found for |- ( ( ph /\ p e. X ) -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) ) with typecode |-
202	201	ralbidva	Could not format ( ph -> ( A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) ) : No typesetting found for |- ( ph -> ( A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) ) with typecode |-
203	194 202	mpbird	Could not format ( ph -> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) : No typesetting found for |- ( ph -> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) with typecode |-
204		sseq1	Could not format ( a = ( p +no q ) -> ( a C_ b <-> ( p +no q ) C_ b ) ) : No typesetting found for |- ( a = ( p +no q ) -> ( a C_ b <-> ( p +no q ) C_ b ) ) with typecode |-
205	204	rexbidv	Could not format ( a = ( p +no q ) -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) : No typesetting found for |- ( a = ( p +no q ) -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) with typecode |-
206	205	imaeqalov	Could not format ( ( +no Fn ( On X. On ) /\ ( X X. { B } ) C_ ( On X. On ) ) -> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( X X. { B } ) C_ ( On X. On ) ) -> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) with typecode |-
207	7 137 206	sylancr	Could not format ( ph -> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) : No typesetting found for |- ( ph -> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) with typecode |-
208	203 207	mpbird	Could not format ( ph -> A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) : No typesetting found for |- ( ph -> A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) with typecode |-
209		ssintub	$$⊢Y\subseteq \bigcap \left\{y\in \mathrm{On}|Y\subseteq y\right\}$$
210	209 4	sseqtrrid	$$⊢\phi \to Y\subseteq B$$
211	210	sselda	$$⊢\left(\phi \wedge q\in Y\right)\to q\in B$$
212		ssid	$$⊢q\subseteq q$$
213		sseq2	$$⊢s=q\to \left(q\subseteq s\leftrightarrow q\subseteq q\right)$$
214	213	rspcev	$$⊢\left(q\in B\wedge q\subseteq q\right)\to \exists s\in Bq\subseteq s$$
215	211 212 214	sylancl	$$⊢\left(\phi \wedge q\in Y\right)\to \exists s\in Bq\subseteq s$$
216	215	ralrimiva	$$⊢\phi \to \forall q\in Y\exists s\in Bq\subseteq s$$
217	92	rexbidv	Could not format ( r = A -> ( E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( r = A -> ( E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
218	217	rexsng	Could not format ( A e. On -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( A e. On -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
219	1 218	syl	Could not format ( ph -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ph -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
220	219	adantr	Could not format ( ( ph /\ q e. Y ) -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ( ph /\ q e. Y ) -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
221		sseq2	Could not format ( b = ( r +no s ) -> ( ( A +no q ) C_ b <-> ( A +no q ) C_ ( r +no s ) ) ) : No typesetting found for |- ( b = ( r +no s ) -> ( ( A +no q ) C_ b <-> ( A +no q ) C_ ( r +no s ) ) ) with typecode |-
222	221	imaeqexov	Could not format ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) ) with typecode |-
223	7 106 222	sylancr	Could not format ( ph -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ph -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) ) with typecode |-
224	223	adantr	Could not format ( ( ph /\ q e. Y ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) ) : No typesetting found for |- ( ( ph /\ q e. Y ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) ) with typecode |-
225	76	sselda	$$⊢\left(\phi \wedge q\in Y\right)\to q\in \mathrm{On}$$
226	225	adantr	$$⊢\left(\left(\phi \wedge q\in Y\right)\wedge s\in B\right)\to q\in \mathrm{On}$$
227	67	adantr	$$⊢\left(\phi \wedge q\in Y\right)\to B\subseteq \mathrm{On}$$
228	227	sselda	$$⊢\left(\left(\phi \wedge q\in Y\right)\wedge s\in B\right)\to s\in \mathrm{On}$$
229	1	ad2antrr	$$⊢\left(\left(\phi \wedge q\in Y\right)\wedge s\in B\right)\to A\in \mathrm{On}$$
230	226 228 229 80	syl3anc	Could not format ( ( ( ph /\ q e. Y ) /\ s e. B ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ( ( ph /\ q e. Y ) /\ s e. B ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
231	230	rexbidva	Could not format ( ( ph /\ q e. Y ) -> ( E. s e. B q C_ s <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) : No typesetting found for |- ( ( ph /\ q e. Y ) -> ( E. s e. B q C_ s <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) ) with typecode |-
232	220 224 231	3bitr4d	Could not format ( ( ph /\ q e. Y ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. s e. B q C_ s ) ) : No typesetting found for |- ( ( ph /\ q e. Y ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. s e. B q C_ s ) ) with typecode |-
233	232	ralbidva	Could not format ( ph -> ( A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> A. q e. Y E. s e. B q C_ s ) ) : No typesetting found for |- ( ph -> ( A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> A. q e. Y E. s e. B q C_ s ) ) with typecode |-
234	216 233	mpbird	Could not format ( ph -> A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b ) : No typesetting found for |- ( ph -> A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b ) with typecode |-
235		orc	Could not format ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) with typecode |-
236	235	ralimi	Could not format ( A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b -> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b -> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) with typecode |-
237	234 236	syl	Could not format ( ph -> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( ph -> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) with typecode |-
238		rexun	Could not format ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) with typecode |-
239	238	ralbii	Could not format ( A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b <-> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b <-> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) ) with typecode |-
240	237 239	sylibr	Could not format ( ph -> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) : No typesetting found for |- ( ph -> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) with typecode |-
241	111	sseq1d	Could not format ( p = A -> ( ( p +no q ) C_ b <-> ( A +no q ) C_ b ) ) : No typesetting found for |- ( p = A -> ( ( p +no q ) C_ b <-> ( A +no q ) C_ b ) ) with typecode |-
242	241	rexbidv	Could not format ( p = A -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( p = A -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) ) with typecode |-
243	242	ralbidv	Could not format ( p = A -> ( A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( p = A -> ( A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) ) with typecode |-
244	243	ralsng	Could not format ( A e. On -> ( A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( A e. On -> ( A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) ) with typecode |-
245	1 244	syl	Could not format ( ph -> ( A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) ) : No typesetting found for |- ( ph -> ( A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) ) with typecode |-
246	240 245	mpbird	Could not format ( ph -> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) : No typesetting found for |- ( ph -> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) with typecode |-
247	205	imaeqalov	Could not format ( ( +no Fn ( On X. On ) /\ ( { A } X. Y ) C_ ( On X. On ) ) -> ( A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( { A } X. Y ) C_ ( On X. On ) ) -> ( A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) with typecode |-
248	7 87 247	sylancr	Could not format ( ph -> ( A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) : No typesetting found for |- ( ph -> ( A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) ) with typecode |-
249	246 248	mpbird	Could not format ( ph -> A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) : No typesetting found for |- ( ph -> A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) with typecode |-
250		ralunb	Could not format ( A. a e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b /\ A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) ) : No typesetting found for |- ( A. a e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b /\ A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) ) with typecode |-
251	208 249 250	sylanbrc	Could not format ( ph -> A. a e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) : No typesetting found for |- ( ph -> A. a e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) with typecode |-
252	32 64 168 251	cofon2	Could not format ( ph -> |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } = |^| { z e. On | ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) C_ z } ) : No typesetting found for |- ( ph -> |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } = |^| { z e. On | ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) C_ z } ) with typecode |-
253	6 252	eqtrd	Could not format ( ph -> ( A +no B ) = |^| { z e. On | ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) C_ z } ) : No typesetting found for |- ( ph -> ( A +no B ) = |^| { z e. On | ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) C_ z } ) with typecode |-