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