Metamath Proof Explorer


Theorem naddcllem

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

Ref Expression
Assertion naddcllem
|- ( ( 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 ) } ) )

Proof

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