Theorem naddasslem2

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

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