Theorem naddasslem1

Description: Lemma for naddass . Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Assertion	naddasslem1	Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = |^| { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		naddcl	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On ) with typecode |-
2	1	3adant3	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no B ) e. On ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no B ) e. On ) with typecode |-
3		simp3	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to C\in \mathrm{On}$$
4		naddov3	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { a e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ a } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { a e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ a } ) with typecode |-
5	4	3adant3	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no B ) = |^| { a e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ a } ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no B ) = |^| { a e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ a } ) with typecode |-
6		intmin	$$⊢C\in \mathrm{On}\to \bigcap \left\{c\in \mathrm{On}|C\subseteq c\right\}=C$$
7	6	eqcomd	$$⊢C\in \mathrm{On}\to C=\bigcap \left\{c\in \mathrm{On}|C\subseteq c\right\}$$
8	7	3ad2ant3	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to C=\bigcap \left\{c\in \mathrm{On}|C\subseteq c\right\}$$
9	2 3 5 8	naddunif	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = |^| { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = |^| { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } ) with typecode |-
10		df-3an	Could not format ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) ) : No typesetting found for |- ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) ) with typecode |-
11		unss	Could not format ( ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x ) <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) C_ x ) : No typesetting found for |- ( ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x ) <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) C_ x ) with typecode |-
12		ancom	Could not format ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x ) ) : No typesetting found for |- ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x ) ) with typecode |-
13		xpundir	Could not format ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) = ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) ) : No typesetting found for |- ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) = ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) ) with typecode |-
14	13	imaeq2i	Could not format ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) = ( +no " ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) : No typesetting found for |- ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) = ( +no " ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) with typecode |-
15		imaundi	Could not format ( +no " ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) = ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) : No typesetting found for |- ( +no " ( ( ( +no " ( { A } X. B ) ) X. { C } ) u. ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) = ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) with typecode |-
16	14 15	eqtri	Could not format ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) = ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) : No typesetting found for |- ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) = ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) with typecode |-
17	16	sseq1i	Could not format ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) C_ x ) : No typesetting found for |- ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x <-> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) u. ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) ) C_ x ) with typecode |-
18	11 12 17	3bitr4i	Could not format ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) <-> ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x ) : No typesetting found for |- ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) <-> ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x ) with typecode |-
19	18	anbi1i	Could not format ( ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) ) : No typesetting found for |- ( ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x ) /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) ) with typecode |-
20		unss	Could not format ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x ) : No typesetting found for |- ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x ) with typecode |-
21	10 19 20	3bitrri	Could not format ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x <-> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) ) : No typesetting found for |- ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x <-> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) ) with typecode |-
22		naddfn	Could not format +no Fn ( On X. On ) : No typesetting found for |- +no Fn ( On X. On ) with typecode |-
23		fnfun	Could not format ( +no Fn ( On X. On ) -> Fun +no ) : No typesetting found for |- ( +no Fn ( On X. On ) -> Fun +no ) with typecode |-
24	22 23	ax-mp	Could not format Fun +no : No typesetting found for |- Fun +no with typecode |-
25		imassrn	Could not format ( +no " ( A X. { B } ) ) C_ ran +no : No typesetting found for |- ( +no " ( A X. { B } ) ) C_ ran +no with typecode |-
26		naddf	Could not format +no : ( On X. On ) --> On : No typesetting found for |- +no : ( On X. On ) --> On with typecode |-
27		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 |-
28	26 27	ax-mp	Could not format ran +no C_ On : No typesetting found for |- ran +no C_ On with typecode |-
29	25 28	sstri	Could not format ( +no " ( A X. { B } ) ) C_ On : No typesetting found for |- ( +no " ( A X. { B } ) ) C_ On with typecode |-
30		simpl3	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to C\in \mathrm{On}$$
31	30	snssd	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to \left\{C\right\}\subseteq \mathrm{On}$$
32		xpss12	Could not format ( ( ( +no " ( A X. { B } ) ) C_ On /\ { C } C_ On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ ( On X. On ) ) : No typesetting found for |- ( ( ( +no " ( A X. { B } ) ) C_ On /\ { C } C_ On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ ( On X. On ) ) with typecode |-
33	29 31 32	sylancr	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ ( On X. On ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ ( On X. On ) ) with typecode |-
34	22	fndmi	Could not format dom +no = ( On X. On ) : No typesetting found for |- dom +no = ( On X. On ) with typecode |-
35	33 34	sseqtrrdi	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ dom +no ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( A X. { B } ) ) X. { C } ) C_ dom +no ) with typecode |-
36		funimassov	Could not format ( ( Fun +no /\ ( ( +no " ( A X. { B } ) ) X. { C } ) C_ dom +no ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x ) ) : No typesetting found for |- ( ( Fun +no /\ ( ( +no " ( A X. { B } ) ) X. { C } ) C_ dom +no ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x ) ) with typecode |-
37	24 35 36	sylancr	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x ) ) with typecode |-
38		oveq2	Could not format ( c = C -> ( p +no c ) = ( p +no C ) ) : No typesetting found for |- ( c = C -> ( p +no c ) = ( p +no C ) ) with typecode |-
39	38	eleq1d	Could not format ( c = C -> ( ( p +no c ) e. x <-> ( p +no C ) e. x ) ) : No typesetting found for |- ( c = C -> ( ( p +no c ) e. x <-> ( p +no C ) e. x ) ) with typecode |-
40	39	ralsng	Could not format ( C e. On -> ( A. c e. { C } ( p +no c ) e. x <-> ( p +no C ) e. x ) ) : No typesetting found for |- ( C e. On -> ( A. c e. { C } ( p +no c ) e. x <-> ( p +no C ) e. x ) ) with typecode |-
41	30 40	syl	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. c e. { C } ( p +no c ) e. x <-> ( p +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. c e. { C } ( p +no c ) e. x <-> ( p +no C ) e. x ) ) with typecode |-
42	41	ralbidv	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x <-> A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) A. c e. { C } ( p +no c ) e. x <-> A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x ) ) with typecode |-
43		onss	$$⊢A\in \mathrm{On}\to A\subseteq \mathrm{On}$$
44	43	3ad2ant1	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to A\subseteq \mathrm{On}$$
45	44	adantr	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to A\subseteq \mathrm{On}$$
46		simpl2	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to B\in \mathrm{On}$$
47	46	snssd	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to \left\{B\right\}\subseteq \mathrm{On}$$
48		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}$$
49	45 47 48	syl2anc	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to A\times \left\{B\right\}\subseteq \mathrm{On}\times \mathrm{On}$$
50		oveq1	Could not format ( p = ( a +no b ) -> ( p +no C ) = ( ( a +no b ) +no C ) ) : No typesetting found for |- ( p = ( a +no b ) -> ( p +no C ) = ( ( a +no b ) +no C ) ) with typecode |-
51	50	eleq1d	Could not format ( p = ( a +no b ) -> ( ( p +no C ) e. x <-> ( ( a +no b ) +no C ) e. x ) ) : No typesetting found for |- ( p = ( a +no b ) -> ( ( p +no C ) e. x <-> ( ( a +no b ) +no C ) e. x ) ) with typecode |-
52	51	imaeqalov	Could not format ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x ) ) with typecode |-
53	22 49 52	sylancr	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x ) ) with typecode |-
54		oveq2	Could not format ( b = B -> ( a +no b ) = ( a +no B ) ) : No typesetting found for |- ( b = B -> ( a +no b ) = ( a +no B ) ) with typecode |-
55	54	oveq1d	Could not format ( b = B -> ( ( a +no b ) +no C ) = ( ( a +no B ) +no C ) ) : No typesetting found for |- ( b = B -> ( ( a +no b ) +no C ) = ( ( a +no B ) +no C ) ) with typecode |-
56	55	eleq1d	Could not format ( b = B -> ( ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) ) : No typesetting found for |- ( b = B -> ( ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) ) with typecode |-
57	56	ralsng	Could not format ( B e. On -> ( A. b e. { B } ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) ) : No typesetting found for |- ( B e. On -> ( A. b e. { B } ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) ) with typecode |-
58	46 57	syl	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. b e. { B } ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. b e. { B } ( ( a +no b ) +no C ) e. x <-> ( ( a +no B ) +no C ) e. x ) ) with typecode |-
59	58	ralbidv	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. a e. A A. b e. { B } ( ( a +no b ) +no C ) e. x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) ) with typecode |-
60	53 59	bitrd	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( A X. { B } ) ) ( p +no C ) e. x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) ) with typecode |-
61	37 42 60	3bitrd	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x <-> A. a e. A ( ( a +no B ) +no C ) e. x ) ) with typecode |-
62		imassrn	Could not format ( +no " ( { A } X. B ) ) C_ ran +no : No typesetting found for |- ( +no " ( { A } X. B ) ) C_ ran +no with typecode |-
63	62 28	sstri	Could not format ( +no " ( { A } X. B ) ) C_ On : No typesetting found for |- ( +no " ( { A } X. B ) ) C_ On with typecode |-
64		xpss12	Could not format ( ( ( +no " ( { A } X. B ) ) C_ On /\ { C } C_ On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ ( On X. On ) ) : No typesetting found for |- ( ( ( +no " ( { A } X. B ) ) C_ On /\ { C } C_ On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ ( On X. On ) ) with typecode |-
65	63 31 64	sylancr	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ ( On X. On ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ ( On X. On ) ) with typecode |-
66	65 34	sseqtrrdi	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ dom +no ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { A } X. B ) ) X. { C } ) C_ dom +no ) with typecode |-
67		funimassov	Could not format ( ( Fun +no /\ ( ( +no " ( { A } X. B ) ) X. { C } ) C_ dom +no ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x ) ) : No typesetting found for |- ( ( Fun +no /\ ( ( +no " ( { A } X. B ) ) X. { C } ) C_ dom +no ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x ) ) with typecode |-
68	24 66 67	sylancr	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x ) ) with typecode |-
69	41	ralbidv	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x <-> A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) A. c e. { C } ( p +no c ) e. x <-> A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x ) ) with typecode |-
70		simpl1	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to A\in \mathrm{On}$$
71	70	snssd	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to \left\{A\right\}\subseteq \mathrm{On}$$
72		onss	$$⊢B\in \mathrm{On}\to B\subseteq \mathrm{On}$$
73	72	3ad2ant2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to B\subseteq \mathrm{On}$$
74	73	adantr	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to B\subseteq \mathrm{On}$$
75		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}$$
76	71 74 75	syl2anc	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to \left\{A\right\}\times B\subseteq \mathrm{On}\times \mathrm{On}$$
77	51	imaeqalov	Could not format ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x ) ) : No typesetting found for |- ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x ) ) with typecode |-
78	22 76 77	sylancr	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x ) ) with typecode |-
79		oveq1	Could not format ( a = A -> ( a +no b ) = ( A +no b ) ) : No typesetting found for |- ( a = A -> ( a +no b ) = ( A +no b ) ) with typecode |-
80	79	oveq1d	Could not format ( a = A -> ( ( a +no b ) +no C ) = ( ( A +no b ) +no C ) ) : No typesetting found for |- ( a = A -> ( ( a +no b ) +no C ) = ( ( A +no b ) +no C ) ) with typecode |-
81	80	eleq1d	Could not format ( a = A -> ( ( ( a +no b ) +no C ) e. x <-> ( ( A +no b ) +no C ) e. x ) ) : No typesetting found for |- ( a = A -> ( ( ( a +no b ) +no C ) e. x <-> ( ( A +no b ) +no C ) e. x ) ) with typecode |-
82	81	ralbidv	Could not format ( a = A -> ( A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) : No typesetting found for |- ( a = A -> ( A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) with typecode |-
83	82	ralsng	Could not format ( A e. On -> ( A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) : No typesetting found for |- ( A e. On -> ( A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) with typecode |-
84	70 83	syl	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. a e. { A } A. b e. B ( ( a +no b ) +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) with typecode |-
85	78 84	bitrd	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A. p e. ( +no " ( { A } X. B ) ) ( p +no C ) e. x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) with typecode |-
86	68 69 85	3bitrd	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x <-> A. b e. B ( ( A +no b ) +no C ) e. x ) ) with typecode |-
87	2	adantr	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A +no B ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( A +no B ) e. On ) with typecode |-
88	87	snssd	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { ( A +no B ) } C_ On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> { ( A +no B ) } C_ On ) with typecode |-
89		onss	$$⊢C\in \mathrm{On}\to C\subseteq \mathrm{On}$$
90	89	3ad2ant3	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to C\subseteq \mathrm{On}$$
91	90	adantr	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge x\in \mathrm{On}\right)\to C\subseteq \mathrm{On}$$
92		xpss12	Could not format ( ( { ( A +no B ) } C_ On /\ C C_ On ) -> ( { ( A +no B ) } X. C ) C_ ( On X. On ) ) : No typesetting found for |- ( ( { ( A +no B ) } C_ On /\ C C_ On ) -> ( { ( A +no B ) } X. C ) C_ ( On X. On ) ) with typecode |-
93	88 91 92	syl2anc	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { ( A +no B ) } X. C ) C_ ( On X. On ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { ( A +no B ) } X. C ) C_ ( On X. On ) ) with typecode |-
94	93 34	sseqtrrdi	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { ( A +no B ) } X. C ) C_ dom +no ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( { ( A +no B ) } X. C ) C_ dom +no ) with typecode |-
95		funimassov	Could not format ( ( Fun +no /\ ( { ( A +no B ) } X. C ) C_ dom +no ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x ) ) : No typesetting found for |- ( ( Fun +no /\ ( { ( A +no B ) } X. C ) C_ dom +no ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x ) ) with typecode |-
96	24 94 95	sylancr	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x ) ) with typecode |-
97		ovex	Could not format ( A +no B ) e. _V : No typesetting found for |- ( A +no B ) e. _V with typecode |-
98		oveq1	Could not format ( a = ( A +no B ) -> ( a +no c ) = ( ( A +no B ) +no c ) ) : No typesetting found for |- ( a = ( A +no B ) -> ( a +no c ) = ( ( A +no B ) +no c ) ) with typecode |-
99	98	eleq1d	Could not format ( a = ( A +no B ) -> ( ( a +no c ) e. x <-> ( ( A +no B ) +no c ) e. x ) ) : No typesetting found for |- ( a = ( A +no B ) -> ( ( a +no c ) e. x <-> ( ( A +no B ) +no c ) e. x ) ) with typecode |-
100	99	ralbidv	Could not format ( a = ( A +no B ) -> ( A. c e. C ( a +no c ) e. x <-> A. c e. C ( ( A +no B ) +no c ) e. x ) ) : No typesetting found for |- ( a = ( A +no B ) -> ( A. c e. C ( a +no c ) e. x <-> A. c e. C ( ( A +no B ) +no c ) e. x ) ) with typecode |-
101	97 100	ralsn	Could not format ( A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x <-> A. c e. C ( ( A +no B ) +no c ) e. x ) : No typesetting found for |- ( A. a e. { ( A +no B ) } A. c e. C ( a +no c ) e. x <-> A. c e. C ( ( A +no B ) +no c ) e. x ) with typecode |-
102	96 101	bitrdi	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. c e. C ( ( A +no B ) +no c ) e. x ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( +no " ( { ( A +no B ) } X. C ) ) C_ x <-> A. c e. C ( ( A +no B ) +no c ) e. x ) ) with typecode |-
103	61 86 102	3anbi123d	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( ( +no " ( ( +no " ( A X. { B } ) ) X. { C } ) ) C_ x /\ ( +no " ( ( +no " ( { A } X. B ) ) X. { C } ) ) C_ x /\ ( +no " ( { ( A +no B ) } X. C ) ) C_ x ) <-> ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) ) ) with typecode |-
104	21 103	bitrid	Could not format ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x <-> ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ x e. On ) -> ( ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x <-> ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) ) ) with typecode |-
105	104	rabbidva	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } = { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } = { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } ) with typecode |-
106	105	inteqd	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> |^| { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } = |^| { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> |^| { x e. On | ( ( +no " ( ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) X. { C } ) ) u. ( +no " ( { ( A +no B ) } X. C ) ) ) C_ x } = |^| { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } ) with typecode |-
107	9 106	eqtrd	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = |^| { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = |^| { x e. On | ( A. a e. A ( ( a +no B ) +no C ) e. x /\ A. b e. B ( ( A +no b ) +no C ) e. x /\ A. c e. C ( ( A +no B ) +no c ) e. x ) } ) with typecode |-