Theorem naddid1

Description: Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 26-Aug-2024)

	Ref	Expression
Assertion	naddid1	Could not format assertion : No typesetting found for |- ( A e. On -> ( A +no (/) ) = A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( a = b -> ( a +no (/) ) = ( b +no (/) ) ) : No typesetting found for |- ( a = b -> ( a +no (/) ) = ( b +no (/) ) ) with typecode |-
2		id	$$⊢a=b\to a=b$$
3	1 2	eqeq12d	Could not format ( a = b -> ( ( a +no (/) ) = a <-> ( b +no (/) ) = b ) ) : No typesetting found for |- ( a = b -> ( ( a +no (/) ) = a <-> ( b +no (/) ) = b ) ) with typecode |-
4		oveq1	Could not format ( a = A -> ( a +no (/) ) = ( A +no (/) ) ) : No typesetting found for |- ( a = A -> ( a +no (/) ) = ( A +no (/) ) ) with typecode |-
5		id	$$⊢a=A\to a=A$$
6	4 5	eqeq12d	Could not format ( a = A -> ( ( a +no (/) ) = a <-> ( A +no (/) ) = A ) ) : No typesetting found for |- ( a = A -> ( ( a +no (/) ) = a <-> ( A +no (/) ) = A ) ) with typecode |-
7		0elon	$$⊢\varnothing \in \mathrm{On}$$
8		naddov2	Could not format ( ( a e. On /\ (/) e. On ) -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } ) : No typesetting found for |- ( ( a e. On /\ (/) e. On ) -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } ) with typecode |-
9	7 8	mpan2	Could not format ( a e. On -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } ) : No typesetting found for |- ( a e. On -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } ) with typecode |-
10	9	adantr	Could not format ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( a +no (/) ) = |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } ) with typecode |-
11		ral0	Could not format A. c e. (/) ( a +no c ) e. x : No typesetting found for |- A. c e. (/) ( a +no c ) e. x with typecode |-
12	11	biantrur	Could not format ( A. b e. a ( b +no (/) ) e. x <-> ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) ) : No typesetting found for |- ( A. b e. a ( b +no (/) ) e. x <-> ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) ) with typecode |-
13		eleq1	Could not format ( ( b +no (/) ) = b -> ( ( b +no (/) ) e. x <-> b e. x ) ) : No typesetting found for |- ( ( b +no (/) ) = b -> ( ( b +no (/) ) e. x <-> b e. x ) ) with typecode |-
14	13	ralimi	Could not format ( A. b e. a ( b +no (/) ) = b -> A. b e. a ( ( b +no (/) ) e. x <-> b e. x ) ) : No typesetting found for |- ( A. b e. a ( b +no (/) ) = b -> A. b e. a ( ( b +no (/) ) e. x <-> b e. x ) ) with typecode |-
15		ralbi	Could not format ( A. b e. a ( ( b +no (/) ) e. x <-> b e. x ) -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) ) : No typesetting found for |- ( A. b e. a ( ( b +no (/) ) e. x <-> b e. x ) -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) ) with typecode |-
16	14 15	syl	Could not format ( A. b e. a ( b +no (/) ) = b -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) ) : No typesetting found for |- ( A. b e. a ( b +no (/) ) = b -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) ) with typecode |-
17	16	adantl	Could not format ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( A. b e. a ( b +no (/) ) e. x <-> A. b e. a b e. x ) ) with typecode |-
18		dfss3	$$⊢a\subseteq x\leftrightarrow \forall b\in ab\in x$$
19	17 18	bitr4di	Could not format ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( A. b e. a ( b +no (/) ) e. x <-> a C_ x ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( A. b e. a ( b +no (/) ) e. x <-> a C_ x ) ) with typecode |-
20	12 19	bitr3id	Could not format ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) <-> a C_ x ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) <-> a C_ x ) ) with typecode |-
21	20	rabbidv	Could not format ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } = { x e. On | a C_ x } ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } = { x e. On | a C_ x } ) with typecode |-
22	21	inteqd	Could not format ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } = |^| { x e. On | a C_ x } ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> |^| { x e. On | ( A. c e. (/) ( a +no c ) e. x /\ A. b e. a ( b +no (/) ) e. x ) } = |^| { x e. On | a C_ x } ) with typecode |-
23		intmin	$$⊢a\in \mathrm{On}\to \bigcap \left\{x\in \mathrm{On}|a\subseteq x\right\}=a$$
24	23	adantr	Could not format ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> |^| { x e. On | a C_ x } = a ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> |^| { x e. On | a C_ x } = a ) with typecode |-
25	10 22 24	3eqtrd	Could not format ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( a +no (/) ) = a ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b +no (/) ) = b ) -> ( a +no (/) ) = a ) with typecode |-
26	25	ex	Could not format ( a e. On -> ( A. b e. a ( b +no (/) ) = b -> ( a +no (/) ) = a ) ) : No typesetting found for |- ( a e. On -> ( A. b e. a ( b +no (/) ) = b -> ( a +no (/) ) = a ) ) with typecode |-
27	3 6 26	tfis3	Could not format ( A e. On -> ( A +no (/) ) = A ) : No typesetting found for |- ( A e. On -> ( A +no (/) ) = A ) with typecode |-