Theorem naddov2

Description: Alternate expression for natural addition. (Contributed by Scott Fenton, 26-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		naddov	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) with typecode |-
2		snssi	$$⊢A\in \mathrm{On}\to \left\{A\right\}\subseteq \mathrm{On}$$
3		onss	$$⊢B\in \mathrm{On}\to B\subseteq \mathrm{On}$$
4		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}$$
5	2 3 4	syl2an	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left\{A\right\}\times B\subseteq \mathrm{On}\times \mathrm{On}$$
6		naddfn	Could not format +no Fn ( On X. On ) : No typesetting found for |- +no Fn ( On X. On ) with typecode |-
7	6	fndmi	Could not format dom +no = ( On X. On ) : No typesetting found for |- dom +no = ( On X. On ) with typecode |-
8	5 7	sseqtrrdi	Could not format ( ( A e. On /\ B e. On ) -> ( { A } X. B ) C_ dom +no ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( { A } X. B ) C_ dom +no ) with typecode |-
9		fnfun	Could not format ( +no Fn ( On X. On ) -> Fun +no ) : No typesetting found for |- ( +no Fn ( On X. On ) -> Fun +no ) with typecode |-
10	6 9	ax-mp	Could not format Fun +no : No typesetting found for |- Fun +no with typecode |-
11		funimassov	Could not format ( ( Fun +no /\ ( { A } X. B ) C_ dom +no ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) ) : No typesetting found for |- ( ( Fun +no /\ ( { A } X. B ) C_ dom +no ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) ) with typecode |-
12	10 11	mpan	Could not format ( ( { A } X. B ) C_ dom +no -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) ) : No typesetting found for |- ( ( { A } X. B ) C_ dom +no -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) ) with typecode |-
13	8 12	syl	Could not format ( ( A e. On /\ B e. On ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. t e. { A } A. y e. B ( t +no y ) e. x ) ) with typecode |-
14		oveq1	Could not format ( t = A -> ( t +no y ) = ( A +no y ) ) : No typesetting found for |- ( t = A -> ( t +no y ) = ( A +no y ) ) with typecode |-
15	14	eleq1d	Could not format ( t = A -> ( ( t +no y ) e. x <-> ( A +no y ) e. x ) ) : No typesetting found for |- ( t = A -> ( ( t +no y ) e. x <-> ( A +no y ) e. x ) ) with typecode |-
16	15	ralbidv	Could not format ( t = A -> ( A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) ) : No typesetting found for |- ( t = A -> ( A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) ) with typecode |-
17	16	ralsng	Could not format ( A e. On -> ( A. t e. { A } A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) ) : No typesetting found for |- ( A e. On -> ( A. t e. { A } A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) ) with typecode |-
18	17	adantr	Could not format ( ( A e. On /\ B e. On ) -> ( A. t e. { A } A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A. t e. { A } A. y e. B ( t +no y ) e. x <-> A. y e. B ( A +no y ) e. x ) ) with typecode |-
19	13 18	bitrd	Could not format ( ( A e. On /\ B e. On ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. y e. B ( A +no y ) e. x ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( +no " ( { A } X. B ) ) C_ x <-> A. y e. B ( A +no y ) e. x ) ) with typecode |-
20		onss	$$⊢A\in \mathrm{On}\to A\subseteq \mathrm{On}$$
21		snssi	$$⊢B\in \mathrm{On}\to \left\{B\right\}\subseteq \mathrm{On}$$
22		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}$$
23	20 21 22	syl2an	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A\times \left\{B\right\}\subseteq \mathrm{On}\times \mathrm{On}$$
24	23 7	sseqtrrdi	Could not format ( ( A e. On /\ B e. On ) -> ( A X. { B } ) C_ dom +no ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A X. { B } ) C_ dom +no ) with typecode |-
25		funimassov	Could not format ( ( Fun +no /\ ( A X. { B } ) C_ dom +no ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) ) : No typesetting found for |- ( ( Fun +no /\ ( A X. { B } ) C_ dom +no ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) ) with typecode |-
26	10 25	mpan	Could not format ( ( A X. { B } ) C_ dom +no -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) ) : No typesetting found for |- ( ( A X. { B } ) C_ dom +no -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) ) with typecode |-
27	24 26	syl	Could not format ( ( A e. On /\ B e. On ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A A. t e. { B } ( z +no t ) e. x ) ) with typecode |-
28		oveq2	Could not format ( t = B -> ( z +no t ) = ( z +no B ) ) : No typesetting found for |- ( t = B -> ( z +no t ) = ( z +no B ) ) with typecode |-
29	28	eleq1d	Could not format ( t = B -> ( ( z +no t ) e. x <-> ( z +no B ) e. x ) ) : No typesetting found for |- ( t = B -> ( ( z +no t ) e. x <-> ( z +no B ) e. x ) ) with typecode |-
30	29	ralsng	Could not format ( B e. On -> ( A. t e. { B } ( z +no t ) e. x <-> ( z +no B ) e. x ) ) : No typesetting found for |- ( B e. On -> ( A. t e. { B } ( z +no t ) e. x <-> ( z +no B ) e. x ) ) with typecode |-
31	30	ralbidv	Could not format ( B e. On -> ( A. z e. A A. t e. { B } ( z +no t ) e. x <-> A. z e. A ( z +no B ) e. x ) ) : No typesetting found for |- ( B e. On -> ( A. z e. A A. t e. { B } ( z +no t ) e. x <-> A. z e. A ( z +no B ) e. x ) ) with typecode |-
32	31	adantl	Could not format ( ( A e. On /\ B e. On ) -> ( A. z e. A A. t e. { B } ( z +no t ) e. x <-> A. z e. A ( z +no B ) e. x ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A. z e. A A. t e. { B } ( z +no t ) e. x <-> A. z e. A ( z +no B ) e. x ) ) with typecode |-
33	27 32	bitrd	Could not format ( ( A e. On /\ B e. On ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A ( z +no B ) e. x ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( +no " ( A X. { B } ) ) C_ x <-> A. z e. A ( z +no B ) e. x ) ) with typecode |-
34	19 33	anbi12d	Could not format ( ( A e. On /\ B e. On ) -> ( ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) <-> ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) <-> ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) ) ) with typecode |-
35	34	rabbidv	Could not format ( ( A e. On /\ B e. On ) -> { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } ) with typecode |-
36	35	inteqd	Could not format ( ( A e. On /\ B e. On ) -> |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = |^| { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } = |^| { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } ) with typecode |-
37	1 36	eqtrd	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { x e. On | ( A. y e. B ( A +no y ) e. x /\ A. z e. A ( z +no B ) e. x ) } ) with typecode |-