Theorem naddcllem

Description: Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( a = c -> ( a +no b ) = ( c +no b ) ) : No typesetting found for |- ( a = c -> ( a +no b ) = ( c +no b ) ) with typecode |-
2	1	eleq1d	Could not format ( a = c -> ( ( a +no b ) e. On <-> ( c +no b ) e. On ) ) : No typesetting found for |- ( a = c -> ( ( a +no b ) e. On <-> ( c +no b ) e. On ) ) with typecode |-
3		sneq	$$⊢a=c\to \left\{a\right\}=\left\{c\right\}$$
4	3	xpeq1d	$$⊢a=c\to \left\{a\right\}\times b=\left\{c\right\}\times b$$
5	4	imaeq2d	Could not format ( a = c -> ( +no " ( { a } X. b ) ) = ( +no " ( { c } X. b ) ) ) : No typesetting found for |- ( a = c -> ( +no " ( { a } X. b ) ) = ( +no " ( { c } X. b ) ) ) with typecode |-
6	5	sseq1d	Could not format ( a = c -> ( ( +no " ( { a } X. b ) ) C_ x <-> ( +no " ( { c } X. b ) ) C_ x ) ) : No typesetting found for |- ( a = c -> ( ( +no " ( { a } X. b ) ) C_ x <-> ( +no " ( { c } X. b ) ) C_ x ) ) with typecode |-
7		xpeq1	$$⊢a=c\to a\times \left\{b\right\}=c\times \left\{b\right\}$$
8	7	imaeq2d	Could not format ( a = c -> ( +no " ( a X. { b } ) ) = ( +no " ( c X. { b } ) ) ) : No typesetting found for |- ( a = c -> ( +no " ( a X. { b } ) ) = ( +no " ( c X. { b } ) ) ) with typecode |-
9	8	sseq1d	Could not format ( a = c -> ( ( +no " ( a X. { b } ) ) C_ x <-> ( +no " ( c X. { b } ) ) C_ x ) ) : No typesetting found for |- ( a = c -> ( ( +no " ( a X. { b } ) ) C_ x <-> ( +no " ( c X. { b } ) ) C_ x ) ) with typecode |-
10	6 9	anbi12d	Could not format ( a = c -> ( ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) <-> ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) ) ) : No typesetting found for |- ( a = c -> ( ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) <-> ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) ) ) with typecode |-
11	10	rabbidv	Could not format ( a = c -> { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) : No typesetting found for |- ( a = c -> { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) with typecode |-
12	11	inteqd	Could not format ( a = c -> |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) : No typesetting found for |- ( a = c -> |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) with typecode |-
13	1 12	eqeq12d	Could not format ( a = c -> ( ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } <-> ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) ) : No typesetting found for |- ( a = c -> ( ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } <-> ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) ) with typecode |-
14	2 13	anbi12d	Could not format ( a = c -> ( ( ( a +no b ) e. On /\ ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) <-> ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) ) ) : No typesetting found for |- ( a = c -> ( ( ( a +no b ) e. On /\ ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) <-> ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) ) ) with typecode |-
15		oveq2	Could not format ( b = d -> ( c +no b ) = ( c +no d ) ) : No typesetting found for |- ( b = d -> ( c +no b ) = ( c +no d ) ) with typecode |-
16	15	eleq1d	Could not format ( b = d -> ( ( c +no b ) e. On <-> ( c +no d ) e. On ) ) : No typesetting found for |- ( b = d -> ( ( c +no b ) e. On <-> ( c +no d ) e. On ) ) with typecode |-
17		xpeq2	$$⊢b=d\to \left\{c\right\}\times b=\left\{c\right\}\times d$$
18	17	imaeq2d	Could not format ( b = d -> ( +no " ( { c } X. b ) ) = ( +no " ( { c } X. d ) ) ) : No typesetting found for |- ( b = d -> ( +no " ( { c } X. b ) ) = ( +no " ( { c } X. d ) ) ) with typecode |-
19	18	sseq1d	Could not format ( b = d -> ( ( +no " ( { c } X. b ) ) C_ x <-> ( +no " ( { c } X. d ) ) C_ x ) ) : No typesetting found for |- ( b = d -> ( ( +no " ( { c } X. b ) ) C_ x <-> ( +no " ( { c } X. d ) ) C_ x ) ) with typecode |-
20		sneq	$$⊢b=d\to \left\{b\right\}=\left\{d\right\}$$
21	20	xpeq2d	$$⊢b=d\to c\times \left\{b\right\}=c\times \left\{d\right\}$$
22	21	imaeq2d	Could not format ( b = d -> ( +no " ( c X. { b } ) ) = ( +no " ( c X. { d } ) ) ) : No typesetting found for |- ( b = d -> ( +no " ( c X. { b } ) ) = ( +no " ( c X. { d } ) ) ) with typecode |-
23	22	sseq1d	Could not format ( b = d -> ( ( +no " ( c X. { b } ) ) C_ x <-> ( +no " ( c X. { d } ) ) C_ x ) ) : No typesetting found for |- ( b = d -> ( ( +no " ( c X. { b } ) ) C_ x <-> ( +no " ( c X. { d } ) ) C_ x ) ) with typecode |-
24	19 23	anbi12d	Could not format ( b = d -> ( ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) <-> ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) ) ) : No typesetting found for |- ( b = d -> ( ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) <-> ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) ) ) with typecode |-
25	24	rabbidv	Could not format ( b = d -> { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) : No typesetting found for |- ( b = d -> { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) with typecode |-
26	25	inteqd	Could not format ( b = d -> |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) : No typesetting found for |- ( b = d -> |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) with typecode |-
27	15 26	eqeq12d	Could not format ( b = d -> ( ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } <-> ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) ) : No typesetting found for |- ( b = d -> ( ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } <-> ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) ) with typecode |-
28	16 27	anbi12d	Could not format ( b = d -> ( ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) <-> ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) ) ) : No typesetting found for |- ( b = d -> ( ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) <-> ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) ) ) with typecode |-
29		oveq1	Could not format ( a = c -> ( a +no d ) = ( c +no d ) ) : No typesetting found for |- ( a = c -> ( a +no d ) = ( c +no d ) ) with typecode |-
30	29	eleq1d	Could not format ( a = c -> ( ( a +no d ) e. On <-> ( c +no d ) e. On ) ) : No typesetting found for |- ( a = c -> ( ( a +no d ) e. On <-> ( c +no d ) e. On ) ) with typecode |-
31	3	xpeq1d	$$⊢a=c\to \left\{a\right\}\times d=\left\{c\right\}\times d$$
32	31	imaeq2d	Could not format ( a = c -> ( +no " ( { a } X. d ) ) = ( +no " ( { c } X. d ) ) ) : No typesetting found for |- ( a = c -> ( +no " ( { a } X. d ) ) = ( +no " ( { c } X. d ) ) ) with typecode |-
33	32	sseq1d	Could not format ( a = c -> ( ( +no " ( { a } X. d ) ) C_ x <-> ( +no " ( { c } X. d ) ) C_ x ) ) : No typesetting found for |- ( a = c -> ( ( +no " ( { a } X. d ) ) C_ x <-> ( +no " ( { c } X. d ) ) C_ x ) ) with typecode |-
34		xpeq1	$$⊢a=c\to a\times \left\{d\right\}=c\times \left\{d\right\}$$
35	34	imaeq2d	Could not format ( a = c -> ( +no " ( a X. { d } ) ) = ( +no " ( c X. { d } ) ) ) : No typesetting found for |- ( a = c -> ( +no " ( a X. { d } ) ) = ( +no " ( c X. { d } ) ) ) with typecode |-
36	35	sseq1d	Could not format ( a = c -> ( ( +no " ( a X. { d } ) ) C_ x <-> ( +no " ( c X. { d } ) ) C_ x ) ) : No typesetting found for |- ( a = c -> ( ( +no " ( a X. { d } ) ) C_ x <-> ( +no " ( c X. { d } ) ) C_ x ) ) with typecode |-
37	33 36	anbi12d	Could not format ( a = c -> ( ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) <-> ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) ) ) : No typesetting found for |- ( a = c -> ( ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) <-> ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) ) ) with typecode |-
38	37	rabbidv	Could not format ( a = c -> { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } = { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) : No typesetting found for |- ( a = c -> { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } = { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) with typecode |-
39	38	inteqd	Could not format ( a = c -> |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) : No typesetting found for |- ( a = c -> |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) with typecode |-
40	29 39	eqeq12d	Could not format ( a = c -> ( ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } <-> ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) ) : No typesetting found for |- ( a = c -> ( ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } <-> ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) ) with typecode |-
41	30 40	anbi12d	Could not format ( a = c -> ( ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) <-> ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) ) ) : No typesetting found for |- ( a = c -> ( ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) <-> ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) ) ) with typecode |-
42		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 |-
43	42	eleq1d	Could not format ( a = A -> ( ( a +no b ) e. On <-> ( A +no b ) e. On ) ) : No typesetting found for |- ( a = A -> ( ( a +no b ) e. On <-> ( A +no b ) e. On ) ) with typecode |-
44		sneq	$$⊢a=A\to \left\{a\right\}=\left\{A\right\}$$
45	44	xpeq1d	$$⊢a=A\to \left\{a\right\}\times b=\left\{A\right\}\times b$$
46	45	imaeq2d	Could not format ( a = A -> ( +no " ( { a } X. b ) ) = ( +no " ( { A } X. b ) ) ) : No typesetting found for |- ( a = A -> ( +no " ( { a } X. b ) ) = ( +no " ( { A } X. b ) ) ) with typecode |-
47	46	sseq1d	Could not format ( a = A -> ( ( +no " ( { a } X. b ) ) C_ x <-> ( +no " ( { A } X. b ) ) C_ x ) ) : No typesetting found for |- ( a = A -> ( ( +no " ( { a } X. b ) ) C_ x <-> ( +no " ( { A } X. b ) ) C_ x ) ) with typecode |-
48		xpeq1	$$⊢a=A\to a\times \left\{b\right\}=A\times \left\{b\right\}$$
49	48	imaeq2d	Could not format ( a = A -> ( +no " ( a X. { b } ) ) = ( +no " ( A X. { b } ) ) ) : No typesetting found for |- ( a = A -> ( +no " ( a X. { b } ) ) = ( +no " ( A X. { b } ) ) ) with typecode |-
50	49	sseq1d	Could not format ( a = A -> ( ( +no " ( a X. { b } ) ) C_ x <-> ( +no " ( A X. { b } ) ) C_ x ) ) : No typesetting found for |- ( a = A -> ( ( +no " ( a X. { b } ) ) C_ x <-> ( +no " ( A X. { b } ) ) C_ x ) ) with typecode |-
51	47 50	anbi12d	Could not format ( a = A -> ( ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) <-> ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) ) ) : No typesetting found for |- ( a = A -> ( ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) <-> ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) ) ) with typecode |-
52	51	rabbidv	Could not format ( a = A -> { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) : No typesetting found for |- ( a = A -> { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) with typecode |-
53	52	inteqd	Could not format ( a = A -> |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) : No typesetting found for |- ( a = A -> |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) with typecode |-
54	42 53	eqeq12d	Could not format ( a = A -> ( ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } <-> ( A +no b ) = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) ) : No typesetting found for |- ( a = A -> ( ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } <-> ( A +no b ) = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) ) with typecode |-
55	43 54	anbi12d	Could not format ( a = A -> ( ( ( a +no b ) e. On /\ ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) <-> ( ( A +no 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 = A -> ( ( ( a +no b ) e. On /\ ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) <-> ( ( A +no b ) e. On /\ ( A +no b ) = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) ) ) with typecode |-
56		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 |-
57	56	eleq1d	Could not format ( b = B -> ( ( A +no b ) e. On <-> ( A +no B ) e. On ) ) : No typesetting found for |- ( b = B -> ( ( A +no b ) e. On <-> ( A +no B ) e. On ) ) with typecode |-
58		xpeq2	$$⊢b=B\to \left\{A\right\}\times b=\left\{A\right\}\times B$$
59	58	imaeq2d	Could not format ( b = B -> ( +no " ( { A } X. b ) ) = ( +no " ( { A } X. B ) ) ) : No typesetting found for |- ( b = B -> ( +no " ( { A } X. b ) ) = ( +no " ( { A } X. B ) ) ) with typecode |-
60	59	sseq1d	Could not format ( b = B -> ( ( +no " ( { A } X. b ) ) C_ x <-> ( +no " ( { A } X. B ) ) C_ x ) ) : No typesetting found for |- ( b = B -> ( ( +no " ( { A } X. b ) ) C_ x <-> ( +no " ( { A } X. B ) ) C_ x ) ) with typecode |-
61		sneq	$$⊢b=B\to \left\{b\right\}=\left\{B\right\}$$
62	61	xpeq2d	$$⊢b=B\to A\times \left\{b\right\}=A\times \left\{B\right\}$$
63	62	imaeq2d	Could not format ( b = B -> ( +no " ( A X. { b } ) ) = ( +no " ( A X. { B } ) ) ) : No typesetting found for |- ( b = B -> ( +no " ( A X. { b } ) ) = ( +no " ( A X. { B } ) ) ) with typecode |-
64	63	sseq1d	Could not format ( b = B -> ( ( +no " ( A X. { b } ) ) C_ x <-> ( +no " ( A X. { B } ) ) C_ x ) ) : No typesetting found for |- ( b = B -> ( ( +no " ( A X. { b } ) ) C_ x <-> ( +no " ( A X. { B } ) ) C_ x ) ) with typecode |-
65	60 64	anbi12d	Could not format ( b = B -> ( ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) <-> ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) ) ) : No typesetting found for |- ( b = B -> ( ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) <-> ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) ) ) with typecode |-
66	65	rabbidv	Could not format ( b = B -> { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) : No typesetting found for |- ( b = B -> { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) with typecode |-
67	66	inteqd	Could not format ( b = B -> |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) : No typesetting found for |- ( b = B -> |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) with typecode |-
68	56 67	eqeq12d	Could not format ( b = B -> ( ( A +no b ) = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } <-> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) ) : No typesetting found for |- ( b = B -> ( ( A +no b ) = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } <-> ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) ) with typecode |-
69	57 68	anbi12d	Could not format ( b = B -> ( ( ( A +no b ) e. On /\ ( A +no b ) = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) <-> ( ( A +no 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 |- ( b = B -> ( ( ( A +no b ) e. On /\ ( A +no b ) = |^| { x e. On | ( ( +no " ( { A } X. b ) ) C_ x /\ ( +no " ( A X. { b } ) ) C_ x ) } ) <-> ( ( A +no B ) e. On /\ ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) ) ) with typecode |-
70		simpl	Could not format ( ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) -> ( c +no b ) e. On ) : No typesetting found for |- ( ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) -> ( c +no b ) e. On ) with typecode |-
71	70	ralimi	Could not format ( A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) -> A. c e. a ( c +no b ) e. On ) : No typesetting found for |- ( A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) -> A. c e. a ( c +no b ) e. On ) with typecode |-
72	71	3ad2ant2	Could not format ( ( A. c e. a A. d e. b ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) /\ A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) /\ A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) ) -> A. c e. a ( c +no b ) e. On ) : No typesetting found for |- ( ( A. c e. a A. d e. b ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) /\ A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) /\ A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) ) -> A. c e. a ( c +no b ) e. On ) with typecode |-
73		simpl	Could not format ( ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) -> ( a +no d ) e. On ) : No typesetting found for |- ( ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) -> ( a +no d ) e. On ) with typecode |-
74	73	ralimi	Could not format ( A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) -> A. d e. b ( a +no d ) e. On ) : No typesetting found for |- ( A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) -> A. d e. b ( a +no d ) e. On ) with typecode |-
75	74	3ad2ant3	Could not format ( ( A. c e. a A. d e. b ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) /\ A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) /\ A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) ) -> A. d e. b ( a +no d ) e. On ) : No typesetting found for |- ( ( A. c e. a A. d e. b ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) /\ A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) /\ A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) ) -> A. d e. b ( a +no d ) e. On ) with typecode |-
76	72 75	jca	Could not format ( ( A. c e. a A. d e. b ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) /\ A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) /\ A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) ) -> ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) : No typesetting found for |- ( ( A. c e. a A. d e. b ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) /\ A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) /\ A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) ) -> ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) with typecode |-
77		df-nadd	Could not format +no = frecs ( { <. p , q >. | ( p e. ( On X. On ) /\ q e. ( On X. On ) /\ ( ( ( 1st ` p ) _E ( 1st ` q ) \/ ( 1st ` p ) = ( 1st ` q ) ) /\ ( ( 2nd ` p ) _E ( 2nd ` q ) \/ ( 2nd ` p ) = ( 2nd ` q ) ) /\ p =/= q ) ) } , ( On X. On ) , ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ) : No typesetting found for |- +no = frecs ( { <. p , q >. | ( p e. ( On X. On ) /\ q e. ( On X. On ) /\ ( ( ( 1st ` p ) _E ( 1st ` q ) \/ ( 1st ` p ) = ( 1st ` q ) ) /\ ( ( 2nd ` p ) _E ( 2nd ` q ) \/ ( 2nd ` p ) = ( 2nd ` q ) ) /\ p =/= q ) ) } , ( On X. On ) , ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ) with typecode |-
78	77	on2recsov	Could not format ( ( a e. On /\ b e. On ) -> ( a +no b ) = ( <. a , b >. ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( a +no b ) = ( <. a , b >. ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) ) ) with typecode |-
79	78	adantr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a +no b ) = ( <. a , b >. ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a +no b ) = ( <. a , b >. ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) ) ) with typecode |-
80		opex	$$⊢⟨a,b⟩\in \mathrm{V}$$
81		naddfn	Could not format +no Fn ( On X. On ) : No typesetting found for |- +no Fn ( On X. On ) with typecode |-
82		fnfun	Could not format ( +no Fn ( On X. On ) -> Fun +no ) : No typesetting found for |- ( +no Fn ( On X. On ) -> Fun +no ) with typecode |-
83	81 82	ax-mp	Could not format Fun +no : No typesetting found for |- Fun +no with typecode |-
84		vex	$$⊢a\in \mathrm{V}$$
85	84	sucex	$$⊢\mathrm{suc}a\in \mathrm{V}$$
86		vex	$$⊢b\in \mathrm{V}$$
87	86	sucex	$$⊢\mathrm{suc}b\in \mathrm{V}$$
88	85 87	xpex	$$⊢\mathrm{suc}a\times \mathrm{suc}b\in \mathrm{V}$$
89	88	difexi	$$⊢\left(\mathrm{suc}a\times \mathrm{suc}b\right)\setminus \left\{⟨a,b⟩\right\}\in \mathrm{V}$$
90		resfunexg	Could not format ( ( Fun +no /\ ( ( suc a X. suc b ) \ { <. a , b >. } ) e. _V ) -> ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) e. _V ) : No typesetting found for |- ( ( Fun +no /\ ( ( suc a X. suc b ) \ { <. a , b >. } ) e. _V ) -> ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) e. _V ) with typecode |-
91	83 89 90	mp2an	Could not format ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) e. _V : No typesetting found for |- ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) e. _V with typecode |-
92		eloni	$$⊢b\in \mathrm{On}\to \mathrm{Ord}b$$
93	92	ad2antlr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> Ord b ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> Ord b ) with typecode |-
94		ordirr	$$⊢\mathrm{Ord}b\to \neg b\in b$$
95	93 94	syl	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> -. b e. b ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> -. b e. b ) with typecode |-
96	95	olcd	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( -. a e. { a } \/ -. b e. b ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( -. a e. { a } \/ -. b e. b ) ) with typecode |-
97		ianor	$$⊢\neg \left(a\in \left\{a\right\}\wedge b\in b\right)\leftrightarrow \left(\neg a\in \left\{a\right\}\vee \neg b\in b\right)$$
98		opelxp	$$⊢⟨a,b⟩\in \left(\left\{a\right\}\times b\right)\leftrightarrow \left(a\in \left\{a\right\}\wedge b\in b\right)$$
99	97 98	xchnxbir	$$⊢\neg ⟨a,b⟩\in \left(\left\{a\right\}\times b\right)\leftrightarrow \left(\neg a\in \left\{a\right\}\vee \neg b\in b\right)$$
100	96 99	sylibr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> -. <. a , b >. e. ( { a } X. b ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> -. <. a , b >. e. ( { a } X. b ) ) with typecode |-
101	84	sucid	$$⊢a\in \mathrm{suc}a$$
102		snssi	$$⊢a\in \mathrm{suc}a\to \left\{a\right\}\subseteq \mathrm{suc}a$$
103	101 102	ax-mp	$$⊢\left\{a\right\}\subseteq \mathrm{suc}a$$
104		sssucid	$$⊢b\subseteq \mathrm{suc}b$$
105		xpss12	$$⊢\left(\left\{a\right\}\subseteq \mathrm{suc}a\wedge b\subseteq \mathrm{suc}b\right)\to \left\{a\right\}\times b\subseteq \mathrm{suc}a\times \mathrm{suc}b$$
106	103 104 105	mp2an	$$⊢\left\{a\right\}\times b\subseteq \mathrm{suc}a\times \mathrm{suc}b$$
107		ssdifsn	$$⊢\left\{a\right\}\times b\subseteq \left(\mathrm{suc}a\times \mathrm{suc}b\right)\setminus \left\{⟨a,b⟩\right\}\leftrightarrow \left(\left\{a\right\}\times b\subseteq \mathrm{suc}a\times \mathrm{suc}b\wedge \neg ⟨a,b⟩\in \left(\left\{a\right\}\times b\right)\right)$$
108	106 107	mpbiran	$$⊢\left\{a\right\}\times b\subseteq \left(\mathrm{suc}a\times \mathrm{suc}b\right)\setminus \left\{⟨a,b⟩\right\}\leftrightarrow \neg ⟨a,b⟩\in \left(\left\{a\right\}\times b\right)$$
109	100 108	sylibr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( { a } X. b ) C_ ( ( suc a X. suc b ) \ { <. a , b >. } ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( { a } X. b ) C_ ( ( suc a X. suc b ) \ { <. a , b >. } ) ) with typecode |-
110		resima2	Could not format ( ( { a } X. b ) C_ ( ( suc a X. suc b ) \ { <. a , b >. } ) -> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) = ( +no " ( { a } X. b ) ) ) : No typesetting found for |- ( ( { a } X. b ) C_ ( ( suc a X. suc b ) \ { <. a , b >. } ) -> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) = ( +no " ( { a } X. b ) ) ) with typecode |-
111	109 110	syl	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) = ( +no " ( { a } X. b ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) = ( +no " ( { a } X. b ) ) ) with typecode |-
112	111	sseq1d	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x <-> ( +no " ( { a } X. b ) ) C_ x ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x <-> ( +no " ( { a } X. b ) ) C_ x ) ) with typecode |-
113		eloni	$$⊢a\in \mathrm{On}\to \mathrm{Ord}a$$
114	113	ad2antrr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> Ord a ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> Ord a ) with typecode |-
115		ordirr	$$⊢\mathrm{Ord}a\to \neg a\in a$$
116	114 115	syl	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> -. a e. a ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> -. a e. a ) with typecode |-
117	116	orcd	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( -. a e. a \/ -. b e. { b } ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( -. a e. a \/ -. b e. { b } ) ) with typecode |-
118		ianor	$$⊢\neg \left(a\in a\wedge b\in \left\{b\right\}\right)\leftrightarrow \left(\neg a\in a\vee \neg b\in \left\{b\right\}\right)$$
119		opelxp	$$⊢⟨a,b⟩\in \left(a\times \left\{b\right\}\right)\leftrightarrow \left(a\in a\wedge b\in \left\{b\right\}\right)$$
120	118 119	xchnxbir	$$⊢\neg ⟨a,b⟩\in \left(a\times \left\{b\right\}\right)\leftrightarrow \left(\neg a\in a\vee \neg b\in \left\{b\right\}\right)$$
121	117 120	sylibr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> -. <. a , b >. e. ( a X. { b } ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> -. <. a , b >. e. ( a X. { b } ) ) with typecode |-
122		sssucid	$$⊢a\subseteq \mathrm{suc}a$$
123	86	sucid	$$⊢b\in \mathrm{suc}b$$
124		snssi	$$⊢b\in \mathrm{suc}b\to \left\{b\right\}\subseteq \mathrm{suc}b$$
125	123 124	ax-mp	$$⊢\left\{b\right\}\subseteq \mathrm{suc}b$$
126		xpss12	$$⊢\left(a\subseteq \mathrm{suc}a\wedge \left\{b\right\}\subseteq \mathrm{suc}b\right)\to a\times \left\{b\right\}\subseteq \mathrm{suc}a\times \mathrm{suc}b$$
127	122 125 126	mp2an	$$⊢a\times \left\{b\right\}\subseteq \mathrm{suc}a\times \mathrm{suc}b$$
128		ssdifsn	$$⊢a\times \left\{b\right\}\subseteq \left(\mathrm{suc}a\times \mathrm{suc}b\right)\setminus \left\{⟨a,b⟩\right\}\leftrightarrow \left(a\times \left\{b\right\}\subseteq \mathrm{suc}a\times \mathrm{suc}b\wedge \neg ⟨a,b⟩\in \left(a\times \left\{b\right\}\right)\right)$$
129	127 128	mpbiran	$$⊢a\times \left\{b\right\}\subseteq \left(\mathrm{suc}a\times \mathrm{suc}b\right)\setminus \left\{⟨a,b⟩\right\}\leftrightarrow \neg ⟨a,b⟩\in \left(a\times \left\{b\right\}\right)$$
130	121 129	sylibr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a X. { b } ) C_ ( ( suc a X. suc b ) \ { <. a , b >. } ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a X. { b } ) C_ ( ( suc a X. suc b ) \ { <. a , b >. } ) ) with typecode |-
131		resima2	Could not format ( ( a X. { b } ) C_ ( ( suc a X. suc b ) \ { <. a , b >. } ) -> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) = ( +no " ( a X. { b } ) ) ) : No typesetting found for |- ( ( a X. { b } ) C_ ( ( suc a X. suc b ) \ { <. a , b >. } ) -> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) = ( +no " ( a X. { b } ) ) ) with typecode |-
132	130 131	syl	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) = ( +no " ( a X. { b } ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) = ( +no " ( a X. { b } ) ) ) with typecode |-
133	132	sseq1d	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x <-> ( +no " ( a X. { b } ) ) C_ x ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x <-> ( +no " ( a X. { b } ) ) C_ x ) ) with typecode |-
134	112 133	anbi12d	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) <-> ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) <-> ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) ) ) with typecode |-
135	134	rabbidv	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } = { 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. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } = { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) with typecode |-
136	135	inteqd	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } = |^| { 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. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) with typecode |-
137		simprr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> A. d e. b ( a +no d ) e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> A. d e. b ( a +no d ) e. On ) with typecode |-
138		oveq1	Could not format ( t = a -> ( t +no d ) = ( a +no d ) ) : No typesetting found for |- ( t = a -> ( t +no d ) = ( a +no d ) ) with typecode |-
139	138	eleq1d	Could not format ( t = a -> ( ( t +no d ) e. On <-> ( a +no d ) e. On ) ) : No typesetting found for |- ( t = a -> ( ( t +no d ) e. On <-> ( a +no d ) e. On ) ) with typecode |-
140	139	ralbidv	Could not format ( t = a -> ( A. d e. b ( t +no d ) e. On <-> A. d e. b ( a +no d ) e. On ) ) : No typesetting found for |- ( t = a -> ( A. d e. b ( t +no d ) e. On <-> A. d e. b ( a +no d ) e. On ) ) with typecode |-
141	84 140	ralsn	Could not format ( A. t e. { a } A. d e. b ( t +no d ) e. On <-> A. d e. b ( a +no d ) e. On ) : No typesetting found for |- ( A. t e. { a } A. d e. b ( t +no d ) e. On <-> A. d e. b ( a +no d ) e. On ) with typecode |-
142	137 141	sylibr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> A. t e. { a } A. d e. b ( t +no d ) e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> A. t e. { a } A. d e. b ( t +no d ) e. On ) with typecode |-
143		snssi	$$⊢a\in \mathrm{On}\to \left\{a\right\}\subseteq \mathrm{On}$$
144		onss	$$⊢b\in \mathrm{On}\to b\subseteq \mathrm{On}$$
145		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}$$
146	143 144 145	syl2an	$$⊢\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\to \left\{a\right\}\times b\subseteq \mathrm{On}\times \mathrm{On}$$
147	146	adantr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( { a } X. b ) C_ ( On X. On ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( { a } X. b ) C_ ( On X. On ) ) with typecode |-
148	81	fndmi	Could not format dom +no = ( On X. On ) : No typesetting found for |- dom +no = ( On X. On ) with typecode |-
149	147 148	sseqtrrdi	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( { a } X. b ) C_ dom +no ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( { a } X. b ) C_ dom +no ) with typecode |-
150		funimassov	Could not format ( ( Fun +no /\ ( { a } X. b ) C_ dom +no ) -> ( ( +no " ( { a } X. b ) ) C_ On <-> A. t e. { a } A. d e. b ( t +no d ) e. On ) ) : No typesetting found for |- ( ( Fun +no /\ ( { a } X. b ) C_ dom +no ) -> ( ( +no " ( { a } X. b ) ) C_ On <-> A. t e. { a } A. d e. b ( t +no d ) e. On ) ) with typecode |-
151	83 149 150	sylancr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no " ( { a } X. b ) ) C_ On <-> A. t e. { a } A. d e. b ( t +no d ) e. On ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no " ( { a } X. b ) ) C_ On <-> A. t e. { a } A. d e. b ( t +no d ) e. On ) ) with typecode |-
152	142 151	mpbird	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( +no " ( { a } X. b ) ) C_ On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( +no " ( { a } X. b ) ) C_ On ) with typecode |-
153		simprl	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> A. c e. a ( c +no b ) e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> A. c e. a ( c +no b ) e. On ) with typecode |-
154		oveq2	Could not format ( t = b -> ( c +no t ) = ( c +no b ) ) : No typesetting found for |- ( t = b -> ( c +no t ) = ( c +no b ) ) with typecode |-
155	154	eleq1d	Could not format ( t = b -> ( ( c +no t ) e. On <-> ( c +no b ) e. On ) ) : No typesetting found for |- ( t = b -> ( ( c +no t ) e. On <-> ( c +no b ) e. On ) ) with typecode |-
156	86 155	ralsn	Could not format ( A. t e. { b } ( c +no t ) e. On <-> ( c +no b ) e. On ) : No typesetting found for |- ( A. t e. { b } ( c +no t ) e. On <-> ( c +no b ) e. On ) with typecode |-
157	156	ralbii	Could not format ( A. c e. a A. t e. { b } ( c +no t ) e. On <-> A. c e. a ( c +no b ) e. On ) : No typesetting found for |- ( A. c e. a A. t e. { b } ( c +no t ) e. On <-> A. c e. a ( c +no b ) e. On ) with typecode |-
158	153 157	sylibr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> A. c e. a A. t e. { b } ( c +no t ) e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> A. c e. a A. t e. { b } ( c +no t ) e. On ) with typecode |-
159		onss	$$⊢a\in \mathrm{On}\to a\subseteq \mathrm{On}$$
160		snssi	$$⊢b\in \mathrm{On}\to \left\{b\right\}\subseteq \mathrm{On}$$
161		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}$$
162	159 160 161	syl2an	$$⊢\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\to a\times \left\{b\right\}\subseteq \mathrm{On}\times \mathrm{On}$$
163	162	adantr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a X. { b } ) C_ ( On X. On ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a X. { b } ) C_ ( On X. On ) ) with typecode |-
164	163 148	sseqtrrdi	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a X. { b } ) C_ dom +no ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a X. { b } ) C_ dom +no ) with typecode |-
165		funimassov	Could not format ( ( Fun +no /\ ( a X. { b } ) C_ dom +no ) -> ( ( +no " ( a X. { b } ) ) C_ On <-> A. c e. a A. t e. { b } ( c +no t ) e. On ) ) : No typesetting found for |- ( ( Fun +no /\ ( a X. { b } ) C_ dom +no ) -> ( ( +no " ( a X. { b } ) ) C_ On <-> A. c e. a A. t e. { b } ( c +no t ) e. On ) ) with typecode |-
166	83 164 165	sylancr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no " ( a X. { b } ) ) C_ On <-> A. c e. a A. t e. { b } ( c +no t ) e. On ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no " ( a X. { b } ) ) C_ On <-> A. c e. a A. t e. { b } ( c +no t ) e. On ) ) with typecode |-
167	158 166	mpbird	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( +no " ( a X. { b } ) ) C_ On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( +no " ( a X. { b } ) ) C_ On ) with typecode |-
168	152 167	unssd	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ On ) with typecode |-
169		ssorduni	Could not format ( ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ On -> Ord U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) : No typesetting found for |- ( ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ On -> Ord U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) with typecode |-
170	168 169	syl	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> Ord U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> Ord U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) with typecode |-
171		snex	$$⊢\left\{a\right\}\in \mathrm{V}$$
172	171 86	xpex	$$⊢\left\{a\right\}\times b\in \mathrm{V}$$
173		funimaexg	Could not format ( ( Fun +no /\ ( { a } X. b ) e. _V ) -> ( +no " ( { a } X. b ) ) e. _V ) : No typesetting found for |- ( ( Fun +no /\ ( { a } X. b ) e. _V ) -> ( +no " ( { a } X. b ) ) e. _V ) with typecode |-
174	83 172 173	mp2an	Could not format ( +no " ( { a } X. b ) ) e. _V : No typesetting found for |- ( +no " ( { a } X. b ) ) e. _V with typecode |-
175		snex	$$⊢\left\{b\right\}\in \mathrm{V}$$
176	84 175	xpex	$$⊢a\times \left\{b\right\}\in \mathrm{V}$$
177		funimaexg	Could not format ( ( Fun +no /\ ( a X. { b } ) e. _V ) -> ( +no " ( a X. { b } ) ) e. _V ) : No typesetting found for |- ( ( Fun +no /\ ( a X. { b } ) e. _V ) -> ( +no " ( a X. { b } ) ) e. _V ) with typecode |-
178	83 176 177	mp2an	Could not format ( +no " ( a X. { b } ) ) e. _V : No typesetting found for |- ( +no " ( a X. { b } ) ) e. _V with typecode |-
179	174 178	unex	Could not format ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. _V : No typesetting found for |- ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. _V with typecode |-
180	179	uniex	Could not format U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. _V : No typesetting found for |- U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. _V with typecode |-
181	180	elon	Could not format ( U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On <-> Ord U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) : No typesetting found for |- ( U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On <-> Ord U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) with typecode |-
182	170 181	sylibr	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On ) with typecode |-
183		sucelon	Could not format ( U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On <-> suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On ) : No typesetting found for |- ( U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On <-> suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On ) with typecode |-
184	182 183	sylib	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On ) with typecode |-
185		onsucuni	Could not format ( ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ On -> ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) : No typesetting found for |- ( ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ On -> ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) with typecode |-
186	168 185	syl	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) with typecode |-
187	186	unssad	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( +no " ( { a } X. b ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( +no " ( { a } X. b ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) with typecode |-
188	186	unssbd	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( +no " ( a X. { b } ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( +no " ( a X. { b } ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) with typecode |-
189		sseq2	Could not format ( x = suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) -> ( ( +no " ( { a } X. b ) ) C_ x <-> ( +no " ( { a } X. b ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) ) : No typesetting found for |- ( x = suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) -> ( ( +no " ( { a } X. b ) ) C_ x <-> ( +no " ( { a } X. b ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) ) with typecode |-
190		sseq2	Could not format ( x = suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) -> ( ( +no " ( a X. { b } ) ) C_ x <-> ( +no " ( a X. { b } ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) ) : No typesetting found for |- ( x = suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) -> ( ( +no " ( a X. { b } ) ) C_ x <-> ( +no " ( a X. { b } ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) ) with typecode |-
191	189 190	anbi12d	Could not format ( x = suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) -> ( ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) <-> ( ( +no " ( { a } X. b ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) /\ ( +no " ( a X. { b } ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) ) ) : No typesetting found for |- ( x = suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) -> ( ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) <-> ( ( +no " ( { a } X. b ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) /\ ( +no " ( a X. { b } ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) ) ) with typecode |-
192	191	rspcev	Could not format ( ( suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On /\ ( ( +no " ( { a } X. b ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) /\ ( +no " ( a X. { b } ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) ) -> E. x e. On ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) ) : No typesetting found for |- ( ( suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) e. On /\ ( ( +no " ( { a } X. b ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) /\ ( +no " ( a X. { b } ) ) C_ suc U. ( ( +no " ( { a } X. b ) ) u. ( +no " ( a X. { b } ) ) ) ) ) -> E. x e. On ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) ) with typecode |-
193	184 187 188 192	syl12anc	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> E. 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. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> E. x e. On ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) ) with typecode |-
194		onintrab2	Could not format ( E. x e. On ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) <-> |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } e. On ) : No typesetting found for |- ( E. x e. On ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) <-> |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } e. On ) with typecode |-
195	193 194	sylib	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } e. On ) with typecode |-
196	136 195	eqeltrd	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } e. On ) with typecode |-
197	84 86	op1std	$$⊢t=⟨a,b⟩\to 1^{st}\left(t\right)=a$$
198	197	sneqd	$$⊢t=⟨a,b⟩\to \left\{1^{st}\left(t\right)\right\}=\left\{a\right\}$$
199	84 86	op2ndd	$$⊢t=⟨a,b⟩\to 2^{nd}\left(t\right)=b$$
200	198 199	xpeq12d	$$⊢t=⟨a,b⟩\to \left\{1^{st}\left(t\right)\right\}\times 2^{nd}\left(t\right)=\left\{a\right\}\times b$$
201	200	imaeq2d	$$⊢t=⟨a,b⟩\to f\left[\left\{1^{st}\left(t\right)\right\}\times 2^{nd}\left(t\right)\right]=f\left[\left\{a\right\}\times b\right]$$
202	201	sseq1d	$$⊢t=⟨a,b⟩\to \left(f\left[\left\{1^{st}\left(t\right)\right\}\times 2^{nd}\left(t\right)\right]\subseteq x\leftrightarrow f\left[\left\{a\right\}\times b\right]\subseteq x\right)$$
203	199	sneqd	$$⊢t=⟨a,b⟩\to \left\{2^{nd}\left(t\right)\right\}=\left\{b\right\}$$
204	197 203	xpeq12d	$$⊢t=⟨a,b⟩\to 1^{st}\left(t\right)\times \left\{2^{nd}\left(t\right)\right\}=a\times \left\{b\right\}$$
205	204	imaeq2d	$$⊢t=⟨a,b⟩\to f\left[1^{st}\left(t\right)\times \left\{2^{nd}\left(t\right)\right\}\right]=f\left[a\times \left\{b\right\}\right]$$
206	205	sseq1d	$$⊢t=⟨a,b⟩\to \left(f\left[1^{st}\left(t\right)\times \left\{2^{nd}\left(t\right)\right\}\right]\subseteq x\leftrightarrow f\left[a\times \left\{b\right\}\right]\subseteq x\right)$$
207	202 206	anbi12d	$$⊢t=⟨a,b⟩\to \left(\left(f\left[\left\{1^{st}\left(t\right)\right\}\times 2^{nd}\left(t\right)\right]\subseteq x\wedge f\left[1^{st}\left(t\right)\times \left\{2^{nd}\left(t\right)\right\}\right]\subseteq x\right)\leftrightarrow \left(f\left[\left\{a\right\}\times b\right]\subseteq x\wedge f\left[a\times \left\{b\right\}\right]\subseteq x\right)\right)$$
208	207	rabbidv	$$⊢t=⟨a,b⟩\to \left\{x\in \mathrm{On}|\left(f\left[\left\{1^{st}\left(t\right)\right\}\times 2^{nd}\left(t\right)\right]\subseteq x\wedge f\left[1^{st}\left(t\right)\times \left\{2^{nd}\left(t\right)\right\}\right]\subseteq x\right)\right\}=\left\{x\in \mathrm{On}|\left(f\left[\left\{a\right\}\times b\right]\subseteq x\wedge f\left[a\times \left\{b\right\}\right]\subseteq x\right)\right\}$$
209	208	inteqd	$$⊢t=⟨a,b⟩\to \bigcap \left\{x\in \mathrm{On}|\left(f\left[\left\{1^{st}\left(t\right)\right\}\times 2^{nd}\left(t\right)\right]\subseteq x\wedge f\left[1^{st}\left(t\right)\times \left\{2^{nd}\left(t\right)\right\}\right]\subseteq x\right)\right\}=\bigcap \left\{x\in \mathrm{On}|\left(f\left[\left\{a\right\}\times b\right]\subseteq x\wedge f\left[a\times \left\{b\right\}\right]\subseteq x\right)\right\}$$
210		imaeq1	Could not format ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( f " ( { a } X. b ) ) = ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) ) : No typesetting found for |- ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( f " ( { a } X. b ) ) = ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) ) with typecode |-
211	210	sseq1d	Could not format ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( ( f " ( { a } X. b ) ) C_ x <-> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x ) ) : No typesetting found for |- ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( ( f " ( { a } X. b ) ) C_ x <-> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x ) ) with typecode |-
212		imaeq1	Could not format ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( f " ( a X. { b } ) ) = ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) ) : No typesetting found for |- ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( f " ( a X. { b } ) ) = ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) ) with typecode |-
213	212	sseq1d	Could not format ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( ( f " ( a X. { b } ) ) C_ x <-> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) ) : No typesetting found for |- ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( ( f " ( a X. { b } ) ) C_ x <-> ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) ) with typecode |-
214	211 213	anbi12d	Could not format ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( ( ( f " ( { a } X. b ) ) C_ x /\ ( f " ( a X. { b } ) ) C_ x ) <-> ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) ) ) : No typesetting found for |- ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> ( ( ( f " ( { a } X. b ) ) C_ x /\ ( f " ( a X. { b } ) ) C_ x ) <-> ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) ) ) with typecode |-
215	214	rabbidv	Could not format ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> { x e. On | ( ( f " ( { a } X. b ) ) C_ x /\ ( f " ( a X. { b } ) ) C_ x ) } = { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } ) : No typesetting found for |- ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> { x e. On | ( ( f " ( { a } X. b ) ) C_ x /\ ( f " ( a X. { b } ) ) C_ x ) } = { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } ) with typecode |-
216	215	inteqd	Could not format ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> |^| { x e. On | ( ( f " ( { a } X. b ) ) C_ x /\ ( f " ( a X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } ) : No typesetting found for |- ( f = ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) -> |^| { x e. On | ( ( f " ( { a } X. b ) ) C_ x /\ ( f " ( a X. { b } ) ) C_ x ) } = |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } ) with typecode |-
217		eqid	$$⊢\left(t\in \mathrm{V},f\in \mathrm{V}⟼\bigcap \left\{x\in \mathrm{On}|\left(f\left[\left\{1^{st}\left(t\right)\right\}\times 2^{nd}\left(t\right)\right]\subseteq x\wedge f\left[1^{st}\left(t\right)\times \left\{2^{nd}\left(t\right)\right\}\right]\subseteq x\right)\right\}\right)=\left(t\in \mathrm{V},f\in \mathrm{V}⟼\bigcap \left\{x\in \mathrm{On}|\left(f\left[\left\{1^{st}\left(t\right)\right\}\times 2^{nd}\left(t\right)\right]\subseteq x\wedge f\left[1^{st}\left(t\right)\times \left\{2^{nd}\left(t\right)\right\}\right]\subseteq x\right)\right\}\right)$$
218	209 216 217	ovmpog	Could not format ( ( <. a , b >. e. _V /\ ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) e. _V /\ |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } e. On ) -> ( <. a , b >. ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) ) = |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } ) : No typesetting found for |- ( ( <. a , b >. e. _V /\ ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) e. _V /\ |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } e. On ) -> ( <. a , b >. ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) ) = |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } ) with typecode |-
219	80 91 196 218	mp3an12i	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( <. a , b >. ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) ) = |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( <. a , b >. ( t e. _V , f e. _V |-> |^| { x e. On | ( ( f " ( { ( 1st ` t ) } X. ( 2nd ` t ) ) ) C_ x /\ ( f " ( ( 1st ` t ) X. { ( 2nd ` t ) } ) ) C_ x ) } ) ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) ) = |^| { x e. On | ( ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( { a } X. b ) ) C_ x /\ ( ( +no |` ( ( suc a X. suc b ) \ { <. a , b >. } ) ) " ( a X. { b } ) ) C_ x ) } ) with typecode |-
220	79 219 136	3eqtrd	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) 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. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) with typecode |-
221	220 195	eqeltrd	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a +no b ) e. On ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( a +no b ) e. On ) with typecode |-
222	221 220	jca	Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( a +no 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. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) ) -> ( ( a +no b ) e. On /\ ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) ) with typecode |-
223	222	ex	Could not format ( ( a e. On /\ b e. On ) -> ( ( A. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) -> ( ( a +no 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. c e. a ( c +no b ) e. On /\ A. d e. b ( a +no d ) e. On ) -> ( ( a +no b ) e. On /\ ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) ) ) with typecode |-
224	76 223	syl5	Could not format ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) /\ A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) /\ A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) ) -> ( ( a +no 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. c e. a A. d e. b ( ( c +no d ) e. On /\ ( c +no d ) = |^| { x e. On | ( ( +no " ( { c } X. d ) ) C_ x /\ ( +no " ( c X. { d } ) ) C_ x ) } ) /\ A. c e. a ( ( c +no b ) e. On /\ ( c +no b ) = |^| { x e. On | ( ( +no " ( { c } X. b ) ) C_ x /\ ( +no " ( c X. { b } ) ) C_ x ) } ) /\ A. d e. b ( ( a +no d ) e. On /\ ( a +no d ) = |^| { x e. On | ( ( +no " ( { a } X. d ) ) C_ x /\ ( +no " ( a X. { d } ) ) C_ x ) } ) ) -> ( ( a +no b ) e. On /\ ( a +no b ) = |^| { x e. On | ( ( +no " ( { a } X. b ) ) C_ x /\ ( +no " ( a X. { b } ) ) C_ x ) } ) ) ) with typecode |-
225	14 28 41 55 69 224	on2ind	Could not format ( ( A e. On /\ B e. On ) -> ( ( A +no 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 ) e. On /\ ( A +no B ) = |^| { x e. On | ( ( +no " ( { A } X. B ) ) C_ x /\ ( +no " ( A X. { B } ) ) C_ x ) } ) ) with typecode |-