Metamath Proof Explorer

Theorem nmulprop

Description: Show closure and value of natural multiplication. (Contributed by Scott Fenton, 2-Jun-2026)

Ref Expression
Assertion nmulprop 
|- ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( p = r -> ( p .no q ) = ( r .no q ) )
2 1 eleq1d 
 |-  ( p = r -> ( ( p .no q ) e. On <-> ( r .no q ) e. On ) )
3 oveq1 
 |-  ( p = r -> ( p .no b ) = ( r .no b ) )
4 3 oveq2d 
 |-  ( p = r -> ( ( a .no q ) +no ( p .no b ) ) = ( ( a .no q ) +no ( r .no b ) ) )
5 4 eleq1d 
 |-  ( p = r -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
6 5 ralbidv 
 |-  ( p = r -> ( A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
7 6 raleqbi1dv 
 |-  ( p = r -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
8 7 rabbidv 
 |-  ( p = r -> { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } )
9 8 inteqd 
 |-  ( p = r -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } )
10 1 9 eqeq12d 
 |-  ( p = r -> ( ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) )
11 2 10 anbi12d 
 |-  ( p = r -> ( ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) )
12 oveq2 
 |-  ( q = s -> ( r .no q ) = ( r .no s ) )
13 12 eleq1d 
 |-  ( q = s -> ( ( r .no q ) e. On <-> ( r .no s ) e. On ) )
14 oveq2 
 |-  ( q = s -> ( a .no q ) = ( a .no s ) )
15 14 oveq1d 
 |-  ( q = s -> ( ( a .no q ) +no ( r .no b ) ) = ( ( a .no s ) +no ( r .no b ) ) )
16 15 eleq1d 
 |-  ( q = s -> ( ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
17 16 raleqbi1dv 
 |-  ( q = s -> ( A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
18 17 ralbidv 
 |-  ( q = s -> ( A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
19 18 rabbidv 
 |-  ( q = s -> { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } )
20 19 inteqd 
 |-  ( q = s -> |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } )
21 12 20 eqeq12d 
 |-  ( q = s -> ( ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) )
22 13 21 anbi12d 
 |-  ( q = s -> ( ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) )
23 oveq1 
 |-  ( p = r -> ( p .no s ) = ( r .no s ) )
24 23 eleq1d 
 |-  ( p = r -> ( ( p .no s ) e. On <-> ( r .no s ) e. On ) )
25 3 oveq2d 
 |-  ( p = r -> ( ( a .no s ) +no ( p .no b ) ) = ( ( a .no s ) +no ( r .no b ) ) )
26 25 eleq1d 
 |-  ( p = r -> ( ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
27 26 ralbidv 
 |-  ( p = r -> ( A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
28 27 raleqbi1dv 
 |-  ( p = r -> ( A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) )
29 28 rabbidv 
 |-  ( p = r -> { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } )
30 29 inteqd 
 |-  ( p = r -> |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } )
31 23 30 eqeq12d 
 |-  ( p = r -> ( ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) )
32 24 31 anbi12d 
 |-  ( p = r -> ( ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) )
33 oveq1 
 |-  ( p = A -> ( p .no q ) = ( A .no q ) )
34 33 eleq1d 
 |-  ( p = A -> ( ( p .no q ) e. On <-> ( A .no q ) e. On ) )
35 oveq1 
 |-  ( p = A -> ( p .no b ) = ( A .no b ) )
36 35 oveq2d 
 |-  ( p = A -> ( ( a .no q ) +no ( p .no b ) ) = ( ( a .no q ) +no ( A .no b ) ) )
37 36 eleq1d 
 |-  ( p = A -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) )
38 37 ralbidv 
 |-  ( p = A -> ( A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) )
39 38 raleqbi1dv 
 |-  ( p = A -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) )
40 39 rabbidv 
 |-  ( p = A -> { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )
41 40 inteqd 
 |-  ( p = A -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )
42 33 41 eqeq12d 
 |-  ( p = A -> ( ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) )
43 34 42 anbi12d 
 |-  ( p = A -> ( ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( A .no q ) e. On /\ ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) )
44 oveq2 
 |-  ( q = B -> ( A .no q ) = ( A .no B ) )
45 44 eleq1d 
 |-  ( q = B -> ( ( A .no q ) e. On <-> ( A .no B ) e. On ) )
46 oveq2 
 |-  ( q = B -> ( a .no q ) = ( a .no B ) )
47 46 oveq1d 
 |-  ( q = B -> ( ( a .no q ) +no ( A .no b ) ) = ( ( a .no B ) +no ( A .no b ) ) )
48 47 eleq1d 
 |-  ( q = B -> ( ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) )
49 48 raleqbi1dv 
 |-  ( q = B -> ( A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) )
50 49 ralbidv 
 |-  ( q = B -> ( A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) )
51 50 rabbidv 
 |-  ( q = B -> { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )
52 51 inteqd 
 |-  ( q = B -> |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )
53 44 52 eqeq12d 
 |-  ( q = B -> ( ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) )
54 45 53 anbi12d 
 |-  ( q = B -> ( ( ( A .no q ) e. On /\ ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) )
55 simpl 
 |-  ( ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( r .no s ) e. On )
56 55 2ralimi 
 |-  ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. r e. p A. s e. q ( r .no s ) e. On )
57 simpl 
 |-  ( ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( r .no q ) e. On )
58 57 ralimi 
 |-  ( A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. r e. p ( r .no q ) e. On )
59 simpl 
 |-  ( ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( p .no s ) e. On )
60 59 ralimi 
 |-  ( A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. s e. q ( p .no s ) e. On )
61 56 58 60 3anim123i 
 |-  ( ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) -> ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) )
62 df-nmul 
 |-  .no = frecs ( { <. t , u >. | ( t e. ( On X. On ) /\ u e. ( On X. On ) /\ ( ( ( 1st ` t ) _E ( 1st ` u ) \/ ( 1st ` t ) = ( 1st ` u ) ) /\ ( ( 2nd ` t ) _E ( 2nd ` u ) \/ ( 2nd ` t ) = ( 2nd ` u ) ) /\ t =/= u ) ) } , ( On X. On ) , ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) )
63 62 on2recsov 
 |-  ( ( p e. On /\ q e. On ) -> ( p .no q ) = ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) )
64 63 adantr 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) = ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) )
65 opex 
 |-  <. p , q >. e. _V
66 nmulfn 
 |-  .no Fn ( On X. On )
67 fnfun 
 |-  ( .no Fn ( On X. On ) -> Fun .no )
68 66 67 ax-mp 
 |-  Fun .no
69 vex 
 |-  p e. _V
70 69 sucex 
 |-  suc p e. _V
71 vex 
 |-  q e. _V
72 71 sucex 
 |-  suc q e. _V
73 70 72 xpex 
 |-  ( suc p X. suc q ) e. _V
74 73 difexi 
 |-  ( ( suc p X. suc q ) \ { <. p , q >. } ) e. _V
75 resfunexg 
 |-  ( ( Fun .no /\ ( ( suc p X. suc q ) \ { <. p , q >. } ) e. _V ) -> ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V )
76 68 74 75 mp2an 
 |-  ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V
77 elelsuc 
 |-  ( a e. p -> a e. suc p )
78 77 adantr 
 |-  ( ( a e. p /\ b e. q ) -> a e. suc p )
79 78 adantl 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> a e. suc p )
80 71 sucid 
 |-  q e. suc q
81 80 a1i 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> q e. suc q )
82 79 81 opelxpd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> <. a , q >. e. ( suc p X. suc q ) )
83 eloni 
 |-  ( p e. On -> Ord p )
84 ordirr 
 |-  ( Ord p -> -. p e. p )
85 elequ1 
 |-  ( a = p -> ( a e. p <-> p e. p ) )
86 85 notbid 
 |-  ( a = p -> ( -. a e. p <-> -. p e. p ) )
87 86 biimprcd 
 |-  ( -. p e. p -> ( a = p -> -. a e. p ) )
88 87 con2d 
 |-  ( -. p e. p -> ( a e. p -> -. a = p ) )
89 83 84 88 3syl 
 |-  ( p e. On -> ( a e. p -> -. a = p ) )
90 89 imp 
 |-  ( ( p e. On /\ a e. p ) -> -. a = p )
91 90 ad2ant2r 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> -. a = p )
92 91 intnanrd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> -. ( a = p /\ q = q ) )
93 opex 
 |-  <. a , q >. e. _V
94 93 elsn 
 |-  ( <. a , q >. e. { <. p , q >. } <-> <. a , q >. = <. p , q >. )
95 vex 
 |-  a e. _V
96 95 71 opth 
 |-  ( <. a , q >. = <. p , q >. <-> ( a = p /\ q = q ) )
97 94 96 bitr2i 
 |-  ( ( a = p /\ q = q ) <-> <. a , q >. e. { <. p , q >. } )
98 92 97 sylnib 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> -. <. a , q >. e. { <. p , q >. } )
99 82 98 eldifd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> <. a , q >. e. ( ( suc p X. suc q ) \ { <. p , q >. } ) )
100 99 fvresd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , q >. ) = ( .no ` <. a , q >. ) )
101 df-ov 
 |-  ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , q >. )
102 df-ov 
 |-  ( a .no q ) = ( .no ` <. a , q >. )
103 100 101 102 3eqtr4g 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) = ( a .no q ) )
104 69 sucid 
 |-  p e. suc p
105 104 a1i 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> p e. suc p )
106 elelsuc 
 |-  ( b e. q -> b e. suc q )
107 106 adantl 
 |-  ( ( a e. p /\ b e. q ) -> b e. suc q )
108 107 adantl 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> b e. suc q )
109 105 108 opelxpd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> <. p , b >. e. ( suc p X. suc q ) )
110 eloni 
 |-  ( q e. On -> Ord q )
111 ordirr 
 |-  ( Ord q -> -. q e. q )
112 elequ1 
 |-  ( b = q -> ( b e. q <-> q e. q ) )
113 112 notbid 
 |-  ( b = q -> ( -. b e. q <-> -. q e. q ) )
114 113 biimprcd 
 |-  ( -. q e. q -> ( b = q -> -. b e. q ) )
115 114 con2d 
 |-  ( -. q e. q -> ( b e. q -> -. b = q ) )
116 110 111 115 3syl 
 |-  ( q e. On -> ( b e. q -> -. b = q ) )
117 116 imp 
 |-  ( ( q e. On /\ b e. q ) -> -. b = q )
118 117 ad2ant2l 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> -. b = q )
119 118 intnand 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> -. ( p = p /\ b = q ) )
120 opex 
 |-  <. p , b >. e. _V
121 120 elsn 
 |-  ( <. p , b >. e. { <. p , q >. } <-> <. p , b >. = <. p , q >. )
122 vex 
 |-  b e. _V
123 69 122 opth 
 |-  ( <. p , b >. = <. p , q >. <-> ( p = p /\ b = q ) )
124 121 123 bitr2i 
 |-  ( ( p = p /\ b = q ) <-> <. p , b >. e. { <. p , q >. } )
125 119 124 sylnib 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> -. <. p , b >. e. { <. p , q >. } )
126 109 125 eldifd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> <. p , b >. e. ( ( suc p X. suc q ) \ { <. p , q >. } ) )
127 126 fvresd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. p , b >. ) = ( .no ` <. p , b >. ) )
128 df-ov 
 |-  ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. p , b >. )
129 df-ov 
 |-  ( p .no b ) = ( .no ` <. p , b >. )
130 127 128 129 3eqtr4g 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( p .no b ) )
131 103 130 oveq12d 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) = ( ( a .no q ) +no ( p .no b ) ) )
132 sssucid 
 |-  p C_ suc p
133 sssucid 
 |-  q C_ suc q
134 xpss12 
 |-  ( ( p C_ suc p /\ q C_ suc q ) -> ( p X. q ) C_ ( suc p X. suc q ) )
135 132 133 134 mp2an 
 |-  ( p X. q ) C_ ( suc p X. suc q )
136 opelxpi 
 |-  ( ( a e. p /\ b e. q ) -> <. a , b >. e. ( p X. q ) )
137 135 136 sselid 
 |-  ( ( a e. p /\ b e. q ) -> <. a , b >. e. ( suc p X. suc q ) )
138 137 adantl 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> <. a , b >. e. ( suc p X. suc q ) )
139 118 intnand 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> -. ( a = p /\ b = q ) )
140 opex 
 |-  <. a , b >. e. _V
141 140 elsn 
 |-  ( <. a , b >. e. { <. p , q >. } <-> <. a , b >. = <. p , q >. )
142 95 122 opth 
 |-  ( <. a , b >. = <. p , q >. <-> ( a = p /\ b = q ) )
143 141 142 bitr2i 
 |-  ( ( a = p /\ b = q ) <-> <. a , b >. e. { <. p , q >. } )
144 139 143 sylnib 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> -. <. a , b >. e. { <. p , q >. } )
145 138 144 eldifd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> <. a , b >. e. ( ( suc p X. suc q ) \ { <. p , q >. } ) )
146 145 fvresd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , b >. ) = ( .no ` <. a , b >. ) )
147 df-ov 
 |-  ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , b >. )
148 df-ov 
 |-  ( a .no b ) = ( .no ` <. a , b >. )
149 146 147 148 3eqtr4g 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( a .no b ) )
150 149 oveq2d 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) = ( x +no ( a .no b ) ) )
151 131 150 eleq12d 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) ) )
152 151 2ralbidva 
 |-  ( ( p e. On /\ q e. On ) -> ( A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) <-> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) ) )
153 152 rabbidv 
 |-  ( ( p e. On /\ q e. On ) -> { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } )
154 153 inteqd 
 |-  ( ( p e. On /\ q e. On ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } )
155 154 adantr 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } )
156 oveq1 
 |-  ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( x +no ( a .no b ) ) = ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) )
157 156 eleq2d 
 |-  ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) )
158 157 2ralbidv 
 |-  ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) )
159 ovex 
 |-  ( ( c .no q ) +no ( p .no d ) ) e. _V
160 71 159 iunex 
 |-  U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. _V
161 160 dfiun2 
 |-  U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) }
162 159 dfiun2 
 |-  U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) }
163 oveq1 
 |-  ( r = c -> ( r .no q ) = ( c .no q ) )
164 163 eleq1d 
 |-  ( r = c -> ( ( r .no q ) e. On <-> ( c .no q ) e. On ) )
165 simplr2 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> A. r e. p ( r .no q ) e. On )
166 165 adantr 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> A. r e. p ( r .no q ) e. On )
167 simplr 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> c e. p )
168 164 166 167 rspcdva 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( c .no q ) e. On )
169 oveq2 
 |-  ( s = d -> ( p .no s ) = ( p .no d ) )
170 169 eleq1d 
 |-  ( s = d -> ( ( p .no s ) e. On <-> ( p .no d ) e. On ) )
171 simplr3 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> A. s e. q ( p .no s ) e. On )
172 171 adantr 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> A. s e. q ( p .no s ) e. On )
173 simpr 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> d e. q )
174 170 172 173 rspcdva 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( p .no d ) e. On )
175 168 174 naddcld 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( ( c .no q ) +no ( p .no d ) ) e. On )
176 eleq1 
 |-  ( x = ( ( c .no q ) +no ( p .no d ) ) -> ( x e. On <-> ( ( c .no q ) +no ( p .no d ) ) e. On ) )
177 175 176 syl5ibrcom 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) )
178 177 rexlimdva 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> ( E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) )
179 178 abssdv 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On )
180 71 abrexex 
 |-  { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. _V
181 180 ssonunii 
 |-  ( { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On )
182 179 181 syl 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On )
183 162 182 eqeltrid 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On )
184 eleq1 
 |-  ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( x e. On <-> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) )
185 183 184 syl5ibrcom 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) )
186 185 rexlimdva 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) )
187 186 abssdv 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On )
188 69 abrexex 
 |-  { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. _V
189 188 ssonunii 
 |-  ( { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On )
190 187 189 syl 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On )
191 161 190 eqeltrid 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On )
192 onsuc 
 |-  ( U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On )
193 191 192 syl 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On )
194 simplr2 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. r e. p ( r .no q ) e. On )
195 164 rspccva 
 |-  ( ( A. r e. p ( r .no q ) e. On /\ c e. p ) -> ( c .no q ) e. On )
196 194 195 sylan 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( c .no q ) e. On )
197 196 adantr 
 |-  ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( c .no q ) e. On )
198 simplr3 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. s e. q ( p .no s ) e. On )
199 198 adantr 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> A. s e. q ( p .no s ) e. On )
200 170 rspccva 
 |-  ( ( A. s e. q ( p .no s ) e. On /\ d e. q ) -> ( p .no d ) e. On )
201 199 200 sylan 
 |-  ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( p .no d ) e. On )
202 197 201 naddcld 
 |-  ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( ( c .no q ) +no ( p .no d ) ) e. On )
203 202 176 syl5ibrcom 
 |-  ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) )
204 203 rexlimdva 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) )
205 204 abssdv 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On )
206 205 181 syl 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On )
207 162 206 eqeltrid 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On )
208 207 184 syl5ibrcom 
 |-  ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) )
209 208 rexlimdva 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) )
210 209 abssdv 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On )
211 210 189 syl 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On )
212 161 211 eqeltrid 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On )
213 212 192 syl 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On )
214 oveq1 
 |-  ( r = a -> ( r .no s ) = ( a .no s ) )
215 214 eleq1d 
 |-  ( r = a -> ( ( r .no s ) e. On <-> ( a .no s ) e. On ) )
216 oveq2 
 |-  ( s = b -> ( a .no s ) = ( a .no b ) )
217 216 eleq1d 
 |-  ( s = b -> ( ( a .no s ) e. On <-> ( a .no b ) e. On ) )
218 simplr1 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. r e. p A. s e. q ( r .no s ) e. On )
219 simprl 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> a e. p )
220 simprr 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> b e. q )
221 215 217 218 219 220 rspc2dv 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( a .no b ) e. On )
222 naddword1 
 |-  ( ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On /\ ( a .no b ) e. On ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) C_ ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) )
223 213 221 222 syl2anc 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) C_ ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) )
224 oveq1 
 |-  ( c = a -> ( c .no q ) = ( a .no q ) )
225 224 oveq1d 
 |-  ( c = a -> ( ( c .no q ) +no ( p .no d ) ) = ( ( a .no q ) +no ( p .no d ) ) )
226 225 iuneq2d 
 |-  ( c = a -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U_ d e. q ( ( a .no q ) +no ( p .no d ) ) )
227 226 sseq2d 
 |-  ( c = a -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) )
228 oveq2 
 |-  ( d = b -> ( p .no d ) = ( p .no b ) )
229 228 oveq2d 
 |-  ( d = b -> ( ( a .no q ) +no ( p .no d ) ) = ( ( a .no q ) +no ( p .no b ) ) )
230 229 sseq2d 
 |-  ( d = b -> ( ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no b ) ) ) )
231 ssidd 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no b ) ) )
232 230 220 231 rspcedvdw 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> E. d e. q ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) )
233 ssiun 
 |-  ( E. d e. q ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) )
234 232 233 syl 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) )
235 227 219 234 rspcedvdw 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> E. c e. p ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) )
236 ssiun 
 |-  ( E. c e. p ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) )
237 235 236 syl 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) )
238 simpr2 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. r e. p ( r .no q ) e. On )
239 simpl 
 |-  ( ( a e. p /\ b e. q ) -> a e. p )
240 oveq1 
 |-  ( r = a -> ( r .no q ) = ( a .no q ) )
241 240 eleq1d 
 |-  ( r = a -> ( ( r .no q ) e. On <-> ( a .no q ) e. On ) )
242 241 rspccva 
 |-  ( ( A. r e. p ( r .no q ) e. On /\ a e. p ) -> ( a .no q ) e. On )
243 238 239 242 syl2an 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( a .no q ) e. On )
244 simpr3 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. s e. q ( p .no s ) e. On )
245 simpr 
 |-  ( ( a e. p /\ b e. q ) -> b e. q )
246 oveq2 
 |-  ( s = b -> ( p .no s ) = ( p .no b ) )
247 246 eleq1d 
 |-  ( s = b -> ( ( p .no s ) e. On <-> ( p .no b ) e. On ) )
248 247 rspccva 
 |-  ( ( A. s e. q ( p .no s ) e. On /\ b e. q ) -> ( p .no b ) e. On )
249 244 245 248 syl2an 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( p .no b ) e. On )
250 243 249 naddcld 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. On )
251 onsssuc 
 |-  ( ( ( ( a .no q ) +no ( p .no b ) ) e. On /\ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) )
252 250 212 251 syl2anc 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) )
253 237 252 mpbid 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) )
254 223 253 sseldd 
 |-  ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) )
255 254 ralrimivva 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) )
256 158 193 255 rspcedvdw 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> E. x e. On A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) )
257 onintrab2 
 |-  ( E. x e. On A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } e. On )
258 256 257 sylib 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } e. On )
259 155 258 eqeltrd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } e. On )
260 69 71 op1std 
 |-  ( v = <. p , q >. -> ( 1st ` v ) = p )
261 69 71 op2ndd 
 |-  ( v = <. p , q >. -> ( 2nd ` v ) = q )
262 261 csbeq1d 
 |-  ( v = <. p , q >. -> [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = [_ q / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } )
263 260 262 csbeq12dv 
 |-  ( v = <. p , q >. -> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = [_ p / c ]_ [_ q / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } )
264 oveq1 
 |-  ( c = p -> ( c w b ) = ( p w b ) )
265 264 oveq2d 
 |-  ( c = p -> ( ( a w d ) +no ( c w b ) ) = ( ( a w d ) +no ( p w b ) ) )
266 265 eleq1d 
 |-  ( c = p -> ( ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) <-> ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) ) )
267 266 ralbidv 
 |-  ( c = p -> ( A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) <-> A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) ) )
268 267 raleqbi1dv 
 |-  ( c = p -> ( A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) <-> A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) ) )
269 268 rabbidv 
 |-  ( c = p -> { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = { x e. On | A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } )
270 269 inteqd 
 |-  ( c = p -> |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } )
271 270 csbeq2dv 
 |-  ( c = p -> [_ q / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = [_ q / d ]_ |^| { x e. On | A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } )
272 69 271 csbie 
 |-  [_ p / c ]_ [_ q / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = [_ q / d ]_ |^| { x e. On | A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) }
273 oveq2 
 |-  ( d = q -> ( a w d ) = ( a w q ) )
274 273 oveq1d 
 |-  ( d = q -> ( ( a w d ) +no ( p w b ) ) = ( ( a w q ) +no ( p w b ) ) )
275 274 eleq1d 
 |-  ( d = q -> ( ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) ) )
276 275 raleqbi1dv 
 |-  ( d = q -> ( A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) ) )
277 276 ralbidv 
 |-  ( d = q -> ( A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) ) )
278 277 rabbidv 
 |-  ( d = q -> { x e. On | A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } )
279 278 inteqd 
 |-  ( d = q -> |^| { x e. On | A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } )
280 71 279 csbie 
 |-  [_ q / d ]_ |^| { x e. On | A. a e. p A. b e. d ( ( a w d ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) }
281 272 280 eqtri 
 |-  [_ p / c ]_ [_ q / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) }
282 oveq 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( a w q ) = ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) )
283 oveq 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( p w b ) = ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) )
284 282 283 oveq12d 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( ( a w q ) +no ( p w b ) ) = ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) )
285 oveq 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( a w b ) = ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) )
286 285 oveq2d 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( x +no ( a w b ) ) = ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) )
287 284 286 eleq12d 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) )
288 287 2ralbidv 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) )
289 288 rabbidv 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } )
290 289 inteqd 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } )
291 281 290 eqtrid 
 |-  ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> [_ p / c ]_ [_ q / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } )
292 eqid 
 |-  ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) = ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } )
293 263 291 292 ovmpog 
 |-  ( ( <. p , q >. e. _V /\ ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V /\ |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } e. On ) -> ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } )
294 65 76 259 293 mp3an12i 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } )
295 64 294 155 3eqtrd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } )
296 295 258 eqeltrd 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) e. On )
297 296 295 jca 
 |-  ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) )
298 297 ex 
 |-  ( ( p e. On /\ q e. On ) -> ( ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) )
299 61 298 syl5 
 |-  ( ( p e. On /\ q e. On ) -> ( ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) )
300 11 22 32 43 54 299 on2ind 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) )