Metamath Proof Explorer


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 a = c
4 3 xpeq1d a = c a × b = c × 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 a × b = c × b
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 c × b = c × 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 b = d
21 20 xpeq2d b = d c × b = c × d
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 a × d = c × 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 a × d = c × d
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 a = A
45 44 xpeq1d a = A a × b = A × 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 a × b = A × b
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 A × b = A × 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 b = B
62 61 xpeq2d b = B A × b = A × B
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 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 V
85 84 sucex suc a V
86 vex b V
87 86 sucex suc b V
88 85 87 xpex suc a × suc b V
89 88 difexi suc a × suc b a b 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 On 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 Ord b ¬ b 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 ¬ a a b b ¬ a a ¬ b b
98 opelxp a b a × b a a b b
99 97 98 xchnxbir ¬ a b a × b ¬ a a ¬ b b
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 suc a
102 snssi a suc a a suc a
103 101 102 ax-mp a suc a
104 sssucid b suc b
105 xpss12 a suc a b suc b a × b suc a × suc b
106 103 104 105 mp2an a × b suc a × suc b
107 ssdifsn a × b suc a × suc b a b a × b suc a × suc b ¬ a b a × b
108 106 107 mpbiran a × b suc a × suc b a b ¬ a b a × b
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 On 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 Ord a ¬ a 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 ¬ a a b b ¬ a a ¬ b b
119 opelxp a b a × b a a b b
120 118 119 xchnxbir ¬ a b a × b ¬ a a ¬ b b
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 suc a
123 86 sucid b suc b
124 snssi b suc b b suc b
125 123 124 ax-mp b suc b
126 xpss12 a suc a b suc b a × b suc a × suc b
127 122 125 126 mp2an a × b suc a × suc b
128 ssdifsn a × b suc a × suc b a b a × b suc a × suc b ¬ a b a × b
129 127 128 mpbiran a × b suc a × suc b a b ¬ a b a × b
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 On a On
144 onss b On b On
145 xpss12 a On b On a × b On × On
146 143 144 145 syl2an a On b On a × b On × 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 On a On
160 snssi b On b On
161 xpss12 a On b On a × b On × On
162 159 160 161 syl2an a On b On a × b On × 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 a V
172 171 86 xpex a × b 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 b V
176 84 175 xpex a × b 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 1 st t = a
198 197 sneqd t = a b 1 st t = a
199 84 86 op2ndd t = a b 2 nd t = b
200 198 199 xpeq12d t = a b 1 st t × 2 nd t = a × b
201 200 imaeq2d t = a b f 1 st t × 2 nd t = f a × b
202 201 sseq1d t = a b f 1 st t × 2 nd t x f a × b x
203 199 sneqd t = a b 2 nd t = b
204 197 203 xpeq12d t = a b 1 st t × 2 nd t = a × b
205 204 imaeq2d t = a b f 1 st t × 2 nd t = f a × b
206 205 sseq1d t = a b f 1 st t × 2 nd t x f a × b x
207 202 206 anbi12d t = a b f 1 st t × 2 nd t x f 1 st t × 2 nd t x f a × b x f a × b x
208 207 rabbidv t = a b x On | f 1 st t × 2 nd t x f 1 st t × 2 nd t x = x On | f a × b x f a × b x
209 208 inteqd t = a b x On | f 1 st t × 2 nd t x f 1 st t × 2 nd t x = x On | f a × b x f a × b x
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 t V , f V x On | f 1 st t × 2 nd t x f 1 st t × 2 nd t x = t V , f V x On | f 1 st t × 2 nd t x f 1 st t × 2 nd t x
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 |-