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 vsnex 
 |-  { 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 vsnex 
 |-  { 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 onsucb 
 |-  ( 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 ) } ) )