Metamath Proof Explorer

Theorem naddunif

Description: Uniformity theorem for natural addition. If A is the upper bound of X and B is the upper bound of Y , then ( A +no B ) can be expressed in terms of X and Y . (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Hypotheses naddunif.1 
|- ( ph -> A e. On )
naddunif.2 
|- ( ph -> B e. On )
naddunif.3 
|- ( ph -> A = |^| { x e. On | X C_ x } )
naddunif.4 
|- ( ph -> B = |^| { y e. On | Y C_ y } )
Assertion naddunif 
|- ( ph -> ( A +no B ) = |^| { z e. On | ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) C_ z } )

Proof

Step Hyp Ref Expression
1 naddunif.1 
 |-  ( ph -> A e. On )
2 naddunif.2 
 |-  ( ph -> B e. On )
3 naddunif.3 
 |-  ( ph -> A = |^| { x e. On | X C_ x } )
4 naddunif.4 
 |-  ( ph -> B = |^| { y e. On | Y C_ y } )
5 naddov3 
 |-  ( ( A e. On /\ B e. On ) -> ( A +no B ) = |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } )
6 1 2 5 syl2anc 
 |-  ( ph -> ( A +no B ) = |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } )
7 naddfn 
 |-  +no Fn ( On X. On )
8 fnfun 
 |-  ( +no Fn ( On X. On ) -> Fun +no )
9 7 8 ax-mp 
 |-  Fun +no
10 snex 
 |-  { A } e. _V
11 xpexg 
 |-  ( ( { A } e. _V /\ B e. On ) -> ( { A } X. B ) e. _V )
12 10 2 11 sylancr 
 |-  ( ph -> ( { A } X. B ) e. _V )
13 funimaexg 
 |-  ( ( Fun +no /\ ( { A } X. B ) e. _V ) -> ( +no " ( { A } X. B ) ) e. _V )
14 9 12 13 sylancr 
 |-  ( ph -> ( +no " ( { A } X. B ) ) e. _V )
15 imassrn 
 |-  ( +no " ( { A } X. B ) ) C_ ran +no
16 naddf 
 |-  +no : ( On X. On ) --> On
17 frn 
 |-  ( +no : ( On X. On ) --> On -> ran +no C_ On )
18 16 17 ax-mp 
 |-  ran +no C_ On
19 15 18 sstri 
 |-  ( +no " ( { A } X. B ) ) C_ On
20 19 a1i 
 |-  ( ph -> ( +no " ( { A } X. B ) ) C_ On )
21 14 20 elpwd 
 |-  ( ph -> ( +no " ( { A } X. B ) ) e. ~P On )
22 snex 
 |-  { B } e. _V
23 xpexg 
 |-  ( ( A e. On /\ { B } e. _V ) -> ( A X. { B } ) e. _V )
24 1 22 23 sylancl 
 |-  ( ph -> ( A X. { B } ) e. _V )
25 funimaexg 
 |-  ( ( Fun +no /\ ( A X. { B } ) e. _V ) -> ( +no " ( A X. { B } ) ) e. _V )
26 9 24 25 sylancr 
 |-  ( ph -> ( +no " ( A X. { B } ) ) e. _V )
27 imassrn 
 |-  ( +no " ( A X. { B } ) ) C_ ran +no
28 27 18 sstri 
 |-  ( +no " ( A X. { B } ) ) C_ On
29 28 a1i 
 |-  ( ph -> ( +no " ( A X. { B } ) ) C_ On )
30 26 29 elpwd 
 |-  ( ph -> ( +no " ( A X. { B } ) ) e. ~P On )
31 pwuncl 
 |-  ( ( ( +no " ( { A } X. B ) ) e. ~P On /\ ( +no " ( A X. { B } ) ) e. ~P On ) -> ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) e. ~P On )
32 21 30 31 syl2anc 
 |-  ( ph -> ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) e. ~P On )
33 3 1 eqeltrrd 
 |-  ( ph -> |^| { x e. On | X C_ x } e. On )
34 onintrab2 
 |-  ( E. x e. On X C_ x <-> |^| { x e. On | X C_ x } e. On )
35 33 34 sylibr 
 |-  ( ph -> E. x e. On X C_ x )
36 vex 
 |-  x e. _V
37 36 ssex 
 |-  ( X C_ x -> X e. _V )
38 37 rexlimivw 
 |-  ( E. x e. On X C_ x -> X e. _V )
39 35 38 syl 
 |-  ( ph -> X e. _V )
40 xpexg 
 |-  ( ( X e. _V /\ { B } e. _V ) -> ( X X. { B } ) e. _V )
41 39 22 40 sylancl 
 |-  ( ph -> ( X X. { B } ) e. _V )
42 funimaexg 
 |-  ( ( Fun +no /\ ( X X. { B } ) e. _V ) -> ( +no " ( X X. { B } ) ) e. _V )
43 9 41 42 sylancr 
 |-  ( ph -> ( +no " ( X X. { B } ) ) e. _V )
44 imassrn 
 |-  ( +no " ( X X. { B } ) ) C_ ran +no
45 44 18 sstri 
 |-  ( +no " ( X X. { B } ) ) C_ On
46 45 a1i 
 |-  ( ph -> ( +no " ( X X. { B } ) ) C_ On )
47 43 46 elpwd 
 |-  ( ph -> ( +no " ( X X. { B } ) ) e. ~P On )
48 4 2 eqeltrrd 
 |-  ( ph -> |^| { y e. On | Y C_ y } e. On )
49 onintrab2 
 |-  ( E. y e. On Y C_ y <-> |^| { y e. On | Y C_ y } e. On )
50 48 49 sylibr 
 |-  ( ph -> E. y e. On Y C_ y )
51 vex 
 |-  y e. _V
52 51 ssex 
 |-  ( Y C_ y -> Y e. _V )
53 52 rexlimivw 
 |-  ( E. y e. On Y C_ y -> Y e. _V )
54 50 53 syl 
 |-  ( ph -> Y e. _V )
55 xpexg 
 |-  ( ( { A } e. _V /\ Y e. _V ) -> ( { A } X. Y ) e. _V )
56 10 54 55 sylancr 
 |-  ( ph -> ( { A } X. Y ) e. _V )
57 funimaexg 
 |-  ( ( Fun +no /\ ( { A } X. Y ) e. _V ) -> ( +no " ( { A } X. Y ) ) e. _V )
58 9 56 57 sylancr 
 |-  ( ph -> ( +no " ( { A } X. Y ) ) e. _V )
59 imassrn 
 |-  ( +no " ( { A } X. Y ) ) C_ ran +no
60 59 18 sstri 
 |-  ( +no " ( { A } X. Y ) ) C_ On
61 60 a1i 
 |-  ( ph -> ( +no " ( { A } X. Y ) ) C_ On )
62 58 61 elpwd 
 |-  ( ph -> ( +no " ( { A } X. Y ) ) e. ~P On )
63 pwuncl 
 |-  ( ( ( +no " ( X X. { B } ) ) e. ~P On /\ ( +no " ( { A } X. Y ) ) e. ~P On ) -> ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) e. ~P On )
64 47 62 63 syl2anc 
 |-  ( ph -> ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) e. ~P On )
65 2 4 cofonr 
 |-  ( ph -> A. q e. B E. s e. Y q C_ s )
66 onss 
 |-  ( B e. On -> B C_ On )
67 2 66 syl 
 |-  ( ph -> B C_ On )
68 67 sselda 
 |-  ( ( ph /\ q e. B ) -> q e. On )
69 68 adantr 
 |-  ( ( ( ph /\ q e. B ) /\ s e. Y ) -> q e. On )
70 onss 
 |-  ( y e. On -> y C_ On )
71 70 adantl 
 |-  ( ( ph /\ y e. On ) -> y C_ On )
72 sstr 
 |-  ( ( Y C_ y /\ y C_ On ) -> Y C_ On )
73 72 expcom 
 |-  ( y C_ On -> ( Y C_ y -> Y C_ On ) )
74 71 73 syl 
 |-  ( ( ph /\ y e. On ) -> ( Y C_ y -> Y C_ On ) )
75 74 rexlimdva 
 |-  ( ph -> ( E. y e. On Y C_ y -> Y C_ On ) )
76 50 75 mpd 
 |-  ( ph -> Y C_ On )
77 76 adantr 
 |-  ( ( ph /\ q e. B ) -> Y C_ On )
78 77 sselda 
 |-  ( ( ( ph /\ q e. B ) /\ s e. Y ) -> s e. On )
79 1 ad2antrr 
 |-  ( ( ( ph /\ q e. B ) /\ s e. Y ) -> A e. On )
80 naddss2 
 |-  ( ( q e. On /\ s e. On /\ A e. On ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) )
81 69 78 79 80 syl3anc 
 |-  ( ( ( ph /\ q e. B ) /\ s e. Y ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) )
82 81 rexbidva 
 |-  ( ( ph /\ q e. B ) -> ( E. s e. Y q C_ s <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) )
83 82 ralbidva 
 |-  ( ph -> ( A. q e. B E. s e. Y q C_ s <-> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) ) )
84 65 83 mpbid 
 |-  ( ph -> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) )
85 1 snssd 
 |-  ( ph -> { A } C_ On )
86 xpss12 
 |-  ( ( { A } C_ On /\ Y C_ On ) -> ( { A } X. Y ) C_ ( On X. On ) )
87 85 76 86 syl2anc 
 |-  ( ph -> ( { A } X. Y ) C_ ( On X. On ) )
88 sseq2 
 |-  ( d = ( r +no s ) -> ( ( A +no q ) C_ d <-> ( A +no q ) C_ ( r +no s ) ) )
89 88 imaeqexov 
 |-  ( ( +no Fn ( On X. On ) /\ ( { A } X. Y ) C_ ( On X. On ) ) -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) ) )
90 7 87 89 sylancr 
 |-  ( ph -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) ) )
91 oveq1 
 |-  ( r = A -> ( r +no s ) = ( A +no s ) )
92 91 sseq2d 
 |-  ( r = A -> ( ( A +no q ) C_ ( r +no s ) <-> ( A +no q ) C_ ( A +no s ) ) )
93 92 rexbidv 
 |-  ( r = A -> ( E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) )
94 93 rexsng 
 |-  ( A e. On -> ( E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) )
95 1 94 syl 
 |-  ( ph -> ( E. r e. { A } E. s e. Y ( A +no q ) C_ ( r +no s ) <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) )
96 90 95 bitrd 
 |-  ( ph -> ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> E. s e. Y ( A +no q ) C_ ( A +no s ) ) )
97 96 ralbidv 
 |-  ( ph -> ( A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d <-> A. q e. B E. s e. Y ( A +no q ) C_ ( A +no s ) ) )
98 84 97 mpbird 
 |-  ( ph -> A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d )
99 olc 
 |-  ( E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d -> ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) )
100 99 ralimi 
 |-  ( A. q e. B E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d -> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) )
101 98 100 syl 
 |-  ( ph -> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) )
102 rexun 
 |-  ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d <-> ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) )
103 102 ralbii 
 |-  ( A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d <-> A. q e. B ( E. d e. ( +no " ( X X. { B } ) ) ( A +no q ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( A +no q ) C_ d ) )
104 101 103 sylibr 
 |-  ( ph -> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d )
105 xpss12 
 |-  ( ( { A } C_ On /\ B C_ On ) -> ( { A } X. B ) C_ ( On X. On ) )
106 85 67 105 syl2anc 
 |-  ( ph -> ( { A } X. B ) C_ ( On X. On ) )
107 sseq1 
 |-  ( c = ( p +no q ) -> ( c C_ d <-> ( p +no q ) C_ d ) )
108 107 rexbidv 
 |-  ( c = ( p +no q ) -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) )
109 108 imaeqalov 
 |-  ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) )
110 7 106 109 sylancr 
 |-  ( ph -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) )
111 oveq1 
 |-  ( p = A -> ( p +no q ) = ( A +no q ) )
112 111 sseq1d 
 |-  ( p = A -> ( ( p +no q ) C_ d <-> ( A +no q ) C_ d ) )
113 112 rexbidv 
 |-  ( p = A -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) )
114 113 ralbidv 
 |-  ( p = A -> ( A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) )
115 114 ralsng 
 |-  ( A e. On -> ( A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) )
116 1 115 syl 
 |-  ( ph -> ( A. p e. { A } A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) )
117 110 116 bitrd 
 |-  ( ph -> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. q e. B E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( A +no q ) C_ d ) )
118 104 117 mpbird 
 |-  ( ph -> A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d )
119 1 3 cofonr 
 |-  ( ph -> A. p e. A E. r e. X p C_ r )
120 onss 
 |-  ( A e. On -> A C_ On )
121 1 120 syl 
 |-  ( ph -> A C_ On )
122 121 sselda 
 |-  ( ( ph /\ p e. A ) -> p e. On )
123 122 adantr 
 |-  ( ( ( ph /\ p e. A ) /\ r e. X ) -> p e. On )
124 ssintub 
 |-  X C_ |^| { x e. On | X C_ x }
125 3 121 eqsstrrd 
 |-  ( ph -> |^| { x e. On | X C_ x } C_ On )
126 124 125 sstrid 
 |-  ( ph -> X C_ On )
127 126 adantr 
 |-  ( ( ph /\ p e. A ) -> X C_ On )
128 127 sselda 
 |-  ( ( ( ph /\ p e. A ) /\ r e. X ) -> r e. On )
129 2 ad2antrr 
 |-  ( ( ( ph /\ p e. A ) /\ r e. X ) -> B e. On )
130 naddss1 
 |-  ( ( p e. On /\ r e. On /\ B e. On ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) )
131 123 128 129 130 syl3anc 
 |-  ( ( ( ph /\ p e. A ) /\ r e. X ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) )
132 131 rexbidva 
 |-  ( ( ph /\ p e. A ) -> ( E. r e. X p C_ r <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) )
133 132 ralbidva 
 |-  ( ph -> ( A. p e. A E. r e. X p C_ r <-> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) ) )
134 119 133 mpbid 
 |-  ( ph -> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) )
135 2 snssd 
 |-  ( ph -> { B } C_ On )
136 xpss12 
 |-  ( ( X C_ On /\ { B } C_ On ) -> ( X X. { B } ) C_ ( On X. On ) )
137 126 135 136 syl2anc 
 |-  ( ph -> ( X X. { B } ) C_ ( On X. On ) )
138 sseq2 
 |-  ( d = ( r +no s ) -> ( ( p +no B ) C_ d <-> ( p +no B ) C_ ( r +no s ) ) )
139 138 imaeqexov 
 |-  ( ( +no Fn ( On X. On ) /\ ( X X. { B } ) C_ ( On X. On ) ) -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) ) )
140 7 137 139 sylancr 
 |-  ( ph -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) ) )
141 oveq2 
 |-  ( s = B -> ( r +no s ) = ( r +no B ) )
142 141 sseq2d 
 |-  ( s = B -> ( ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) )
143 142 rexsng 
 |-  ( B e. On -> ( E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) )
144 2 143 syl 
 |-  ( ph -> ( E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> ( p +no B ) C_ ( r +no B ) ) )
145 144 rexbidv 
 |-  ( ph -> ( E. r e. X E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) )
146 140 145 bitrd 
 |-  ( ph -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> E. r e. X ( p +no B ) C_ ( r +no B ) ) )
147 146 ralbidv 
 |-  ( ph -> ( A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d <-> A. p e. A E. r e. X ( p +no B ) C_ ( r +no B ) ) )
148 134 147 mpbird 
 |-  ( ph -> A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d )
149 orc 
 |-  ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d -> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) )
150 149 ralimi 
 |-  ( A. p e. A E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d -> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) )
151 148 150 syl 
 |-  ( ph -> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) )
152 rexun 
 |-  ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d <-> ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) )
153 152 ralbii 
 |-  ( A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d <-> A. p e. A ( E. d e. ( +no " ( X X. { B } ) ) ( p +no B ) C_ d \/ E. d e. ( +no " ( { A } X. Y ) ) ( p +no B ) C_ d ) )
154 151 153 sylibr 
 |-  ( ph -> A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d )
155 oveq2 
 |-  ( q = B -> ( p +no q ) = ( p +no B ) )
156 155 sseq1d 
 |-  ( q = B -> ( ( p +no q ) C_ d <-> ( p +no B ) C_ d ) )
157 156 rexbidv 
 |-  ( q = B -> ( E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) )
158 157 ralsng 
 |-  ( B e. On -> ( A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) )
159 2 158 syl 
 |-  ( ph -> ( A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) )
160 159 ralbidv 
 |-  ( ph -> ( A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d <-> A. p e. A E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no B ) C_ d ) )
161 154 160 mpbird 
 |-  ( ph -> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d )
162 xpss12 
 |-  ( ( A C_ On /\ { B } C_ On ) -> ( A X. { B } ) C_ ( On X. On ) )
163 121 135 162 syl2anc 
 |-  ( ph -> ( A X. { B } ) C_ ( On X. On ) )
164 108 imaeqalov 
 |-  ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) )
165 7 163 164 sylancr 
 |-  ( ph -> ( A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> A. p e. A A. q e. { B } E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) ( p +no q ) C_ d ) )
166 161 165 mpbird 
 |-  ( ph -> A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d )
167 ralunb 
 |-  ( A. c e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d <-> ( A. c e. ( +no " ( { A } X. B ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d /\ A. c e. ( +no " ( A X. { B } ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d ) )
168 118 166 167 sylanbrc 
 |-  ( ph -> A. c e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) E. d e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) c C_ d )
169 124 3 sseqtrrid 
 |-  ( ph -> X C_ A )
170 169 sselda 
 |-  ( ( ph /\ p e. X ) -> p e. A )
171 ssid 
 |-  p C_ p
172 sseq2 
 |-  ( r = p -> ( p C_ r <-> p C_ p ) )
173 172 rspcev 
 |-  ( ( p e. A /\ p C_ p ) -> E. r e. A p C_ r )
174 170 171 173 sylancl 
 |-  ( ( ph /\ p e. X ) -> E. r e. A p C_ r )
175 174 ralrimiva 
 |-  ( ph -> A. p e. X E. r e. A p C_ r )
176 126 sselda 
 |-  ( ( ph /\ p e. X ) -> p e. On )
177 176 adantr 
 |-  ( ( ( ph /\ p e. X ) /\ r e. A ) -> p e. On )
178 121 adantr 
 |-  ( ( ph /\ p e. X ) -> A C_ On )
179 178 sselda 
 |-  ( ( ( ph /\ p e. X ) /\ r e. A ) -> r e. On )
180 2 ad2antrr 
 |-  ( ( ( ph /\ p e. X ) /\ r e. A ) -> B e. On )
181 177 179 180 130 syl3anc 
 |-  ( ( ( ph /\ p e. X ) /\ r e. A ) -> ( p C_ r <-> ( p +no B ) C_ ( r +no B ) ) )
182 181 rexbidva 
 |-  ( ( ph /\ p e. X ) -> ( E. r e. A p C_ r <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) )
183 182 ralbidva 
 |-  ( ph -> ( A. p e. X E. r e. A p C_ r <-> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) ) )
184 175 183 mpbid 
 |-  ( ph -> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) )
185 sseq2 
 |-  ( b = ( r +no s ) -> ( ( p +no B ) C_ b <-> ( p +no B ) C_ ( r +no s ) ) )
186 185 imaeqexov 
 |-  ( ( +no Fn ( On X. On ) /\ ( A X. { B } ) C_ ( On X. On ) ) -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) ) )
187 7 163 186 sylancr 
 |-  ( ph -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) ) )
188 144 rexbidv 
 |-  ( ph -> ( E. r e. A E. s e. { B } ( p +no B ) C_ ( r +no s ) <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) )
189 187 188 bitrd 
 |-  ( ph -> ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> E. r e. A ( p +no B ) C_ ( r +no B ) ) )
190 189 ralbidv 
 |-  ( ph -> ( A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b <-> A. p e. X E. r e. A ( p +no B ) C_ ( r +no B ) ) )
191 184 190 mpbird 
 |-  ( ph -> A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b )
192 olc 
 |-  ( E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b -> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) )
193 192 ralimi 
 |-  ( A. p e. X E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b -> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) )
194 191 193 syl 
 |-  ( ph -> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) )
195 155 sseq1d 
 |-  ( q = B -> ( ( p +no q ) C_ b <-> ( p +no B ) C_ b ) )
196 195 rexbidv 
 |-  ( q = B -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) )
197 196 ralsng 
 |-  ( B e. On -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) )
198 2 197 syl 
 |-  ( ph -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) )
199 198 adantr 
 |-  ( ( ph /\ p e. X ) -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b ) )
200 rexun 
 |-  ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no B ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) )
201 199 200 bitrdi 
 |-  ( ( ph /\ p e. X ) -> ( A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) )
202 201 ralbidva 
 |-  ( ph -> ( A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. p e. X ( E. b e. ( +no " ( { A } X. B ) ) ( p +no B ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( p +no B ) C_ b ) ) )
203 194 202 mpbird 
 |-  ( ph -> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b )
204 sseq1 
 |-  ( a = ( p +no q ) -> ( a C_ b <-> ( p +no q ) C_ b ) )
205 204 rexbidv 
 |-  ( a = ( p +no q ) -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) )
206 205 imaeqalov 
 |-  ( ( +no Fn ( On X. On ) /\ ( X X. { B } ) C_ ( On X. On ) ) -> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) )
207 7 137 206 sylancr 
 |-  ( ph -> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. X A. q e. { B } E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) )
208 203 207 mpbird 
 |-  ( ph -> A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b )
209 ssintub 
 |-  Y C_ |^| { y e. On | Y C_ y }
210 209 4 sseqtrrid 
 |-  ( ph -> Y C_ B )
211 210 sselda 
 |-  ( ( ph /\ q e. Y ) -> q e. B )
212 ssid 
 |-  q C_ q
213 sseq2 
 |-  ( s = q -> ( q C_ s <-> q C_ q ) )
214 213 rspcev 
 |-  ( ( q e. B /\ q C_ q ) -> E. s e. B q C_ s )
215 211 212 214 sylancl 
 |-  ( ( ph /\ q e. Y ) -> E. s e. B q C_ s )
216 215 ralrimiva 
 |-  ( ph -> A. q e. Y E. s e. B q C_ s )
217 92 rexbidv 
 |-  ( r = A -> ( E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) )
218 217 rexsng 
 |-  ( A e. On -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) )
219 1 218 syl 
 |-  ( ph -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) )
220 219 adantr 
 |-  ( ( ph /\ q e. Y ) -> ( E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) )
221 sseq2 
 |-  ( b = ( r +no s ) -> ( ( A +no q ) C_ b <-> ( A +no q ) C_ ( r +no s ) ) )
222 221 imaeqexov 
 |-  ( ( +no Fn ( On X. On ) /\ ( { A } X. B ) C_ ( On X. On ) ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) )
223 7 106 222 sylancr 
 |-  ( ph -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) )
224 223 adantr 
 |-  ( ( ph /\ q e. Y ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. r e. { A } E. s e. B ( A +no q ) C_ ( r +no s ) ) )
225 76 sselda 
 |-  ( ( ph /\ q e. Y ) -> q e. On )
226 225 adantr 
 |-  ( ( ( ph /\ q e. Y ) /\ s e. B ) -> q e. On )
227 67 adantr 
 |-  ( ( ph /\ q e. Y ) -> B C_ On )
228 227 sselda 
 |-  ( ( ( ph /\ q e. Y ) /\ s e. B ) -> s e. On )
229 1 ad2antrr 
 |-  ( ( ( ph /\ q e. Y ) /\ s e. B ) -> A e. On )
230 226 228 229 80 syl3anc 
 |-  ( ( ( ph /\ q e. Y ) /\ s e. B ) -> ( q C_ s <-> ( A +no q ) C_ ( A +no s ) ) )
231 230 rexbidva 
 |-  ( ( ph /\ q e. Y ) -> ( E. s e. B q C_ s <-> E. s e. B ( A +no q ) C_ ( A +no s ) ) )
232 220 224 231 3bitr4d 
 |-  ( ( ph /\ q e. Y ) -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> E. s e. B q C_ s ) )
233 232 ralbidva 
 |-  ( ph -> ( A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b <-> A. q e. Y E. s e. B q C_ s ) )
234 216 233 mpbird 
 |-  ( ph -> A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b )
235 orc 
 |-  ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b -> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) )
236 235 ralimi 
 |-  ( A. q e. Y E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b -> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) )
237 234 236 syl 
 |-  ( ph -> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) )
238 rexun 
 |-  ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b <-> ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) )
239 238 ralbii 
 |-  ( A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b <-> A. q e. Y ( E. b e. ( +no " ( { A } X. B ) ) ( A +no q ) C_ b \/ E. b e. ( +no " ( A X. { B } ) ) ( A +no q ) C_ b ) )
240 237 239 sylibr 
 |-  ( ph -> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b )
241 111 sseq1d 
 |-  ( p = A -> ( ( p +no q ) C_ b <-> ( A +no q ) C_ b ) )
242 241 rexbidv 
 |-  ( p = A -> ( E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) )
243 242 ralbidv 
 |-  ( p = A -> ( A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) )
244 243 ralsng 
 |-  ( A e. On -> ( A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) )
245 1 244 syl 
 |-  ( ph -> ( A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b <-> A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( A +no q ) C_ b ) )
246 240 245 mpbird 
 |-  ( ph -> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b )
247 205 imaeqalov 
 |-  ( ( +no Fn ( On X. On ) /\ ( { A } X. Y ) C_ ( On X. On ) ) -> ( A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) )
248 7 87 247 sylancr 
 |-  ( ph -> ( A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> A. p e. { A } A. q e. Y E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) ( p +no q ) C_ b ) )
249 246 248 mpbird 
 |-  ( ph -> A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b )
250 ralunb 
 |-  ( A. a e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b <-> ( A. a e. ( +no " ( X X. { B } ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b /\ A. a e. ( +no " ( { A } X. Y ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b ) )
251 208 249 250 sylanbrc 
 |-  ( ph -> A. a e. ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) E. b e. ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) a C_ b )
252 32 64 168 251 cofon2 
 |-  ( ph -> |^| { w e. On | ( ( +no " ( { A } X. B ) ) u. ( +no " ( A X. { B } ) ) ) C_ w } = |^| { z e. On | ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) C_ z } )
253 6 252 eqtrd 
 |-  ( ph -> ( A +no B ) = |^| { z e. On | ( ( +no " ( X X. { B } ) ) u. ( +no " ( { A } X. Y ) ) ) C_ z } )