Theorem nadddilem4

Description: Lemma for nadddi . Prove the forward implication. (Contributed by Scott Fenton, 3-Aug-2026)

	Ref	Expression
Hypotheses	nadddilem4.1	$$⊢\phi \to A\in \mathrm{On}$$
	nadddilem4.2	$$⊢\phi \to B\in \mathrm{On}$$
	nadddilem4.3	$$⊢\phi \to C\in \mathrm{On}$$
	nadddilem4.4	No typesetting found for |- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) with typecode |-
	nadddilem4.5	No typesetting found for |- ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) ) with typecode |-
	nadddilem4.6	No typesetting found for |- ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) with typecode |-
	nadddilem4.7	No typesetting found for |- ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) ) with typecode |-
	nadddilem4.8	No typesetting found for |- ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) ) with typecode |-
Assertion	nadddilem4	Could not format assertion : No typesetting found for |- ( ph -> ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nadddilem4.1	$$⊢\phi \to A\in \mathrm{On}$$
2		nadddilem4.2	$$⊢\phi \to B\in \mathrm{On}$$
3		nadddilem4.3	$$⊢\phi \to C\in \mathrm{On}$$
4		nadddilem4.4	Could not format ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) : No typesetting found for |- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) with typecode |-
5		nadddilem4.5	Could not format ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) ) : No typesetting found for |- ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) ) with typecode |-
6		nadddilem4.6	Could not format ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) : No typesetting found for |- ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) with typecode |-
7		nadddilem4.7	Could not format ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) ) : No typesetting found for |- ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) ) with typecode |-
8		nadddilem4.8	Could not format ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) ) : No typesetting found for |- ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) ) with typecode |-
9		simprr	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\to y\in \left(B+C\right)$$
10	2 3	naddcld	$$⊢\phi \to B+C\in \mathrm{On}$$
11	10	adantr	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\to B+C\in \mathrm{On}$$
12	11 9	onelond	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\to y\in \mathrm{On}$$
13	2	adantr	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\to B\in \mathrm{On}$$
14	3	adantr	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\to C\in \mathrm{On}$$
15		ltnadd	$$⊢\left(y\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to \left(y\in \left(B+C\right)\leftrightarrow \left(\exists z\in By\subseteq z+C\vee \exists w\in Cy\subseteq B+w\right)\right)$$
16	12 13 14 15	syl3anc	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\to \left(y\in \left(B+C\right)\leftrightarrow \left(\exists z\in By\subseteq z+C\vee \exists w\in Cy\subseteq B+w\right)\right)$$
17	1	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(z\in B\wedge y\subseteq z+C\right)\right)\to A\in \mathrm{On}$$
18	2	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(z\in B\wedge y\subseteq z+C\right)\right)\to B\in \mathrm{On}$$
19	3	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(z\in B\wedge y\subseteq z+C\right)\right)\to C\in \mathrm{On}$$
20		simplrl	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(z\in B\wedge y\subseteq z+C\right)\right)\to x\in A$$
21		simplrr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(z\in B\wedge y\subseteq z+C\right)\right)\to y\in \left(B+C\right)$$
22		simprl	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(z\in B\wedge y\subseteq z+C\right)\right)\to z\in B$$
23		simprr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(z\in B\wedge y\subseteq z+C\right)\right)\to y\subseteq z+C$$
24	4	ad2antrr	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) with typecode |-
25	5	ad2antrr	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) ) with typecode |-
26	7	ad2antrr	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) ) with typecode |-
27	17 18 19 20 21 22 23 24 25 26	nadddilem3	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( z e. B /\ y C_ ( z +no C ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) with typecode |-
28	27	rexlimdvaa	Could not format ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( E. z e. B y C_ ( z +no C ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( E. z e. B y C_ ( z +no C ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) with typecode |-
29	1	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to A\in \mathrm{On}$$
30	3	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to C\in \mathrm{On}$$
31	2	ad2antrr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to B\in \mathrm{On}$$
32		simplrl	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to x\in A$$
33		simplrr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to y\in \left(B+C\right)$$
34	31 30	naddcomd	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to B+C=C+B$$
35	33 34	eleqtrd	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to y\in \left(C+B\right)$$
36		simprl	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to w\in C$$
37		simprr	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to y\subseteq B+w$$
38	30 36	onelond	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to w\in \mathrm{On}$$
39	31 38	naddcomd	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to B+w=w+B$$
40	37 39	sseqtrd	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in \left(B+C\right)\right)\right)\wedge \left(w\in C\wedge y\subseteq B+w\right)\right)\to y\subseteq w+B$$
41		oveq1	Could not format ( d = p -> ( d .no ( B +no C ) ) = ( p .no ( B +no C ) ) ) : No typesetting found for |- ( d = p -> ( d .no ( B +no C ) ) = ( p .no ( B +no C ) ) ) with typecode |-
42		oveq1	Could not format ( d = p -> ( d .no B ) = ( p .no B ) ) : No typesetting found for |- ( d = p -> ( d .no B ) = ( p .no B ) ) with typecode |-
43		oveq1	Could not format ( d = p -> ( d .no C ) = ( p .no C ) ) : No typesetting found for |- ( d = p -> ( d .no C ) = ( p .no C ) ) with typecode |-
44	42 43	oveq12d	Could not format ( d = p -> ( ( d .no B ) +no ( d .no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) : No typesetting found for |- ( d = p -> ( ( d .no B ) +no ( d .no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) with typecode |-
45	41 44	eqeq12d	Could not format ( d = p -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) ) : No typesetting found for |- ( d = p -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) ) with typecode |-
46	45	cbvralvw	Could not format ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) : No typesetting found for |- ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) with typecode |-
47	2 3	naddcomd	$$⊢\phi \to B+C=C+B$$
48	47	adantr	$$⊢\left(\phi \wedge p\in A\right)\to B+C=C+B$$
49	48	oveq2d	Could not format ( ( ph /\ p e. A ) -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) ) with typecode |-
50	1	adantr	$$⊢\left(\phi \wedge p\in A\right)\to A\in \mathrm{On}$$
51		simpr	$$⊢\left(\phi \wedge p\in A\right)\to p\in A$$
52	50 51	onelond	$$⊢\left(\phi \wedge p\in A\right)\to p\in \mathrm{On}$$
53	2	adantr	$$⊢\left(\phi \wedge p\in A\right)\to B\in \mathrm{On}$$
54	52 53	nmulcld	Could not format ( ( ph /\ p e. A ) -> ( p .no B ) e. On ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( p .no B ) e. On ) with typecode |-
55	3	adantr	$$⊢\left(\phi \wedge p\in A\right)\to C\in \mathrm{On}$$
56	52 55	nmulcld	Could not format ( ( ph /\ p e. A ) -> ( p .no C ) e. On ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( p .no C ) e. On ) with typecode |-
57	54 56	naddcomd	Could not format ( ( ph /\ p e. A ) -> ( ( p .no B ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no B ) ) ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( ( p .no B ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no B ) ) ) with typecode |-
58	49 57	eqeq12d	Could not format ( ( ph /\ p e. A ) -> ( ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) with typecode |-
59	58	ralbidva	Could not format ( ph -> ( A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ph -> ( A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) with typecode |-
60	46 59	bitrid	Could not format ( ph -> ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ph -> ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) with typecode |-
61	4 60	mpbid	Could not format ( ph -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) : No typesetting found for |- ( ph -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) with typecode |-
62	61	ad2antrr	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) with typecode |-
63		oveq2	$$⊢f=q\to B+f=B+q$$
64	63	oveq2d	Could not format ( f = q -> ( A .no ( B +no f ) ) = ( A .no ( B +no q ) ) ) : No typesetting found for |- ( f = q -> ( A .no ( B +no f ) ) = ( A .no ( B +no q ) ) ) with typecode |-
65		oveq2	Could not format ( f = q -> ( A .no f ) = ( A .no q ) ) : No typesetting found for |- ( f = q -> ( A .no f ) = ( A .no q ) ) with typecode |-
66	65	oveq2d	Could not format ( f = q -> ( ( A .no B ) +no ( A .no f ) ) = ( ( A .no B ) +no ( A .no q ) ) ) : No typesetting found for |- ( f = q -> ( ( A .no B ) +no ( A .no f ) ) = ( ( A .no B ) +no ( A .no q ) ) ) with typecode |-
67	64 66	eqeq12d	Could not format ( f = q -> ( ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) ) ) : No typesetting found for |- ( f = q -> ( ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) ) ) with typecode |-
68	67	cbvralvw	Could not format ( A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> A. q e. C ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) ) : No typesetting found for |- ( A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> A. q e. C ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) ) with typecode |-
69	2	adantr	$$⊢\left(\phi \wedge q\in C\right)\to B\in \mathrm{On}$$
70	3	adantr	$$⊢\left(\phi \wedge q\in C\right)\to C\in \mathrm{On}$$
71		simpr	$$⊢\left(\phi \wedge q\in C\right)\to q\in C$$
72	70 71	onelond	$$⊢\left(\phi \wedge q\in C\right)\to q\in \mathrm{On}$$
73	69 72	naddcomd	$$⊢\left(\phi \wedge q\in C\right)\to B+q=q+B$$
74	73	oveq2d	Could not format ( ( ph /\ q e. C ) -> ( A .no ( B +no q ) ) = ( A .no ( q +no B ) ) ) : No typesetting found for |- ( ( ph /\ q e. C ) -> ( A .no ( B +no q ) ) = ( A .no ( q +no B ) ) ) with typecode |-
75	1 2	nmulcld	Could not format ( ph -> ( A .no B ) e. On ) : No typesetting found for |- ( ph -> ( A .no B ) e. On ) with typecode |-
76	75	adantr	Could not format ( ( ph /\ q e. C ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( ph /\ q e. C ) -> ( A .no B ) e. On ) with typecode |-
77	1	adantr	$$⊢\left(\phi \wedge q\in C\right)\to A\in \mathrm{On}$$
78	77 72	nmulcld	Could not format ( ( ph /\ q e. C ) -> ( A .no q ) e. On ) : No typesetting found for |- ( ( ph /\ q e. C ) -> ( A .no q ) e. On ) with typecode |-
79	76 78	naddcomd	Could not format ( ( ph /\ q e. C ) -> ( ( A .no B ) +no ( A .no q ) ) = ( ( A .no q ) +no ( A .no B ) ) ) : No typesetting found for |- ( ( ph /\ q e. C ) -> ( ( A .no B ) +no ( A .no q ) ) = ( ( A .no q ) +no ( A .no B ) ) ) with typecode |-
80	74 79	eqeq12d	Could not format ( ( ph /\ q e. C ) -> ( ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) <-> ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) ) : No typesetting found for |- ( ( ph /\ q e. C ) -> ( ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) <-> ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) ) with typecode |-
81	80	ralbidva	Could not format ( ph -> ( A. q e. C ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) <-> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) ) : No typesetting found for |- ( ph -> ( A. q e. C ( A .no ( B +no q ) ) = ( ( A .no B ) +no ( A .no q ) ) <-> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) ) with typecode |-
82	68 81	bitrid	Could not format ( ph -> ( A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) ) : No typesetting found for |- ( ph -> ( A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) ) with typecode |-
83	6 82	mpbid	Could not format ( ph -> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) : No typesetting found for |- ( ph -> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) with typecode |-
84	83	ad2antrr	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. q e. C ( A .no ( q +no B ) ) = ( ( A .no q ) +no ( A .no B ) ) ) with typecode |-
85		oveq1	Could not format ( d = p -> ( d .no ( B +no f ) ) = ( p .no ( B +no f ) ) ) : No typesetting found for |- ( d = p -> ( d .no ( B +no f ) ) = ( p .no ( B +no f ) ) ) with typecode |-
86		oveq1	Could not format ( d = p -> ( d .no f ) = ( p .no f ) ) : No typesetting found for |- ( d = p -> ( d .no f ) = ( p .no f ) ) with typecode |-
87	42 86	oveq12d	Could not format ( d = p -> ( ( d .no B ) +no ( d .no f ) ) = ( ( p .no B ) +no ( p .no f ) ) ) : No typesetting found for |- ( d = p -> ( ( d .no B ) +no ( d .no f ) ) = ( ( p .no B ) +no ( p .no f ) ) ) with typecode |-
88	85 87	eqeq12d	Could not format ( d = p -> ( ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> ( p .no ( B +no f ) ) = ( ( p .no B ) +no ( p .no f ) ) ) ) : No typesetting found for |- ( d = p -> ( ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> ( p .no ( B +no f ) ) = ( ( p .no B ) +no ( p .no f ) ) ) ) with typecode |-
89	63	oveq2d	Could not format ( f = q -> ( p .no ( B +no f ) ) = ( p .no ( B +no q ) ) ) : No typesetting found for |- ( f = q -> ( p .no ( B +no f ) ) = ( p .no ( B +no q ) ) ) with typecode |-
90		oveq2	Could not format ( f = q -> ( p .no f ) = ( p .no q ) ) : No typesetting found for |- ( f = q -> ( p .no f ) = ( p .no q ) ) with typecode |-
91	90	oveq2d	Could not format ( f = q -> ( ( p .no B ) +no ( p .no f ) ) = ( ( p .no B ) +no ( p .no q ) ) ) : No typesetting found for |- ( f = q -> ( ( p .no B ) +no ( p .no f ) ) = ( ( p .no B ) +no ( p .no q ) ) ) with typecode |-
92	89 91	eqeq12d	Could not format ( f = q -> ( ( p .no ( B +no f ) ) = ( ( p .no B ) +no ( p .no f ) ) <-> ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) ) ) : No typesetting found for |- ( f = q -> ( ( p .no ( B +no f ) ) = ( ( p .no B ) +no ( p .no f ) ) <-> ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) ) ) with typecode |-
93	88 92	cbvral2vw	Could not format ( A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> A. p e. A A. q e. C ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) ) : No typesetting found for |- ( A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> A. p e. A A. q e. C ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) ) with typecode |-
94	73	adantrl	$$⊢\left(\phi \wedge \left(p\in A\wedge q\in C\right)\right)\to B+q=q+B$$
95	94	oveq2d	Could not format ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no ( B +no q ) ) = ( p .no ( q +no B ) ) ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no ( B +no q ) ) = ( p .no ( q +no B ) ) ) with typecode |-
96	54	adantrr	Could not format ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no B ) e. On ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no B ) e. On ) with typecode |-
97	52	adantrr	$$⊢\left(\phi \wedge \left(p\in A\wedge q\in C\right)\right)\to p\in \mathrm{On}$$
98	72	adantrl	$$⊢\left(\phi \wedge \left(p\in A\wedge q\in C\right)\right)\to q\in \mathrm{On}$$
99	97 98	nmulcld	Could not format ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no q ) e. On ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( p .no q ) e. On ) with typecode |-
100	96 99	naddcomd	Could not format ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( ( p .no B ) +no ( p .no q ) ) = ( ( p .no q ) +no ( p .no B ) ) ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( ( p .no B ) +no ( p .no q ) ) = ( ( p .no q ) +no ( p .no B ) ) ) with typecode |-
101	95 100	eqeq12d	Could not format ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) <-> ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. C ) ) -> ( ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) <-> ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) ) with typecode |-
102	101	2ralbidva	Could not format ( ph -> ( A. p e. A A. q e. C ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) <-> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ph -> ( A. p e. A A. q e. C ( p .no ( B +no q ) ) = ( ( p .no B ) +no ( p .no q ) ) <-> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) ) with typecode |-
103	93 102	bitrid	Could not format ( ph -> ( A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ph -> ( A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) ) with typecode |-
104	8 103	mpbid	Could not format ( ph -> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) : No typesetting found for |- ( ph -> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) with typecode |-
105	104	ad2antrr	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> A. p e. A A. q e. C ( p .no ( q +no B ) ) = ( ( p .no q ) +no ( p .no B ) ) ) with typecode |-
106	29 30 31 32 35 36 40 62 84 105	nadddilem3	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( C +no B ) ) +no ( A .no y ) ) e. ( ( ( A .no C ) +no ( A .no B ) ) +no ( x .no y ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( C +no B ) ) +no ( A .no y ) ) e. ( ( ( A .no C ) +no ( A .no B ) ) +no ( x .no y ) ) ) with typecode |-
107	34	oveq2d	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( x .no ( B +no C ) ) = ( x .no ( C +no B ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( x .no ( B +no C ) ) = ( x .no ( C +no B ) ) ) with typecode |-
108	107	oveq1d	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) = ( ( x .no ( C +no B ) ) +no ( A .no y ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) = ( ( x .no ( C +no B ) ) +no ( A .no y ) ) ) with typecode |-
109	75	ad2antrr	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( A .no B ) e. On ) with typecode |-
110	1 3	nmulcld	Could not format ( ph -> ( A .no C ) e. On ) : No typesetting found for |- ( ph -> ( A .no C ) e. On ) with typecode |-
111	110	ad2antrr	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( A .no C ) e. On ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( A .no C ) e. On ) with typecode |-
112	109 111	naddcomd	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( A .no B ) +no ( A .no C ) ) = ( ( A .no C ) +no ( A .no B ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( A .no B ) +no ( A .no C ) ) = ( ( A .no C ) +no ( A .no B ) ) ) with typecode |-
113	112	oveq1d	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) = ( ( ( A .no C ) +no ( A .no B ) ) +no ( x .no y ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) = ( ( ( A .no C ) +no ( A .no B ) ) +no ( x .no y ) ) ) with typecode |-
114	106 108 113	3eltr4d	Could not format ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) : No typesetting found for |- ( ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) /\ ( w e. C /\ y C_ ( B +no w ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) with typecode |-
115	114	rexlimdvaa	Could not format ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( E. w e. C y C_ ( B +no w ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( E. w e. C y C_ ( B +no w ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) with typecode |-
116	28 115	jaod	Could not format ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( ( E. z e. B y C_ ( z +no C ) \/ E. w e. C y C_ ( B +no w ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( ( E. z e. B y C_ ( z +no C ) \/ E. w e. C y C_ ( B +no w ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) with typecode |-
117	16 116	sylbid	Could not format ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( y e. ( B +no C ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( y e. ( B +no C ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) with typecode |-
118	9 117	mpd	Could not format ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) : No typesetting found for |- ( ( ph /\ ( x e. A /\ y e. ( B +no C ) ) ) -> ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) with typecode |-
119	118	ralrimivva	Could not format ( ph -> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) : No typesetting found for |- ( ph -> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) with typecode |-
120	75 110	naddcld	Could not format ( ph -> ( ( A .no B ) +no ( A .no C ) ) e. On ) : No typesetting found for |- ( ph -> ( ( A .no B ) +no ( A .no C ) ) e. On ) with typecode |-
121		nmulle	Could not format ( ( A e. On /\ ( B +no C ) e. On /\ ( ( A .no B ) +no ( A .no C ) ) e. On ) -> ( ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) <-> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) : No typesetting found for |- ( ( A e. On /\ ( B +no C ) e. On /\ ( ( A .no B ) +no ( A .no C ) ) e. On ) -> ( ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) <-> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) with typecode |-
122	1 10 120 121	syl3anc	Could not format ( ph -> ( ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) <-> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) : No typesetting found for |- ( ph -> ( ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) <-> A. x e. A A. y e. ( B +no C ) ( ( x .no ( B +no C ) ) +no ( A .no y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( x .no y ) ) ) ) with typecode |-
123	119 122	mpbird	Could not format ( ph -> ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) ) : No typesetting found for |- ( ph -> ( A .no ( B +no C ) ) C_ ( ( A .no B ) +no ( A .no C ) ) ) with typecode |-