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 ⊢ ( 𝜑 → 𝐴 ∈ On )
naddunif.2 ⊢ ( 𝜑 → 𝐵 ∈ On )
naddunif.3 ⊢ ( 𝜑 → 𝐴 = ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } )
naddunif.4 ⊢ ( 𝜑 → 𝐵 = ∩ { 𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦 } )
Assertion naddunif ( 𝜑 → ( 𝐴 +no 𝐵 ) = ∩ { 𝑧 ∈ On ∣ ( ( +no “ ( 𝑋 × { 𝐵 } ) ) ∪ ( +no “ ( { 𝐴 } × 𝑌 ) ) ) ⊆ 𝑧 } )

Proof

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