MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  naddunif Structured version   Visualization version   GIF version

Theorem naddunif 8680
Description: Uniformity theorem for natural addition. If 𝐴 is the upper bound of 𝑋 and 𝐵 is the upper bound of 𝑌, then (𝐴 +no 𝐵) can be expressed in terms of 𝑋 and 𝑌. (Contributed by Scott Fenton, 20-Jan-2025.)
Hypotheses
Ref Expression
naddunif.1 (𝜑𝐴 ∈ On)
naddunif.2 (𝜑𝐵 ∈ On)
naddunif.3 (𝜑𝐴 = {𝑥 ∈ On ∣ 𝑋𝑥})
naddunif.4 (𝜑𝐵 = {𝑦 ∈ On ∣ 𝑌𝑦})
Assertion
Ref Expression
naddunif (𝜑 → (𝐴 +no 𝐵) = {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
Distinct variable groups:   𝑥,𝐴,𝑧   𝑧,𝐵,𝑦   𝑥,𝑋,𝑧   𝑧,𝑌,𝑦   𝜑,𝑥   𝜑,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑦)   𝐵(𝑥)   𝑋(𝑦)   𝑌(𝑥)

Proof of Theorem naddunif
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑟 𝑠 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 naddunif.1 . . 3 (𝜑𝐴 ∈ On)
2 naddunif.2 . . 3 (𝜑𝐵 ∈ On)
3 naddov3 8667 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
41, 2, 3syl2anc 585 . 2 (𝜑 → (𝐴 +no 𝐵) = {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
5 naddfn 8662 . . . . . . 7 +no Fn (On × On)
6 fnfun 6641 . . . . . . 7 ( +no Fn (On × On) → Fun +no )
75, 6ax-mp 5 . . . . . 6 Fun +no
8 snex 5427 . . . . . . 7 {𝐴} ∈ V
9 xpexg 7724 . . . . . . 7 (({𝐴} ∈ V ∧ 𝐵 ∈ On) → ({𝐴} × 𝐵) ∈ V)
108, 2, 9sylancr 588 . . . . . 6 (𝜑 → ({𝐴} × 𝐵) ∈ V)
11 funimaexg 6626 . . . . . 6 ((Fun +no ∧ ({𝐴} × 𝐵) ∈ V) → ( +no “ ({𝐴} × 𝐵)) ∈ V)
127, 10, 11sylancr 588 . . . . 5 (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ V)
13 imassrn 6063 . . . . . . 7 ( +no “ ({𝐴} × 𝐵)) ⊆ ran +no
14 naddf 8668 . . . . . . . 8 +no :(On × On)⟶On
15 frn 6714 . . . . . . . 8 ( +no :(On × On)⟶On → ran +no ⊆ On)
1614, 15ax-mp 5 . . . . . . 7 ran +no ⊆ On
1713, 16sstri 3989 . . . . . 6 ( +no “ ({𝐴} × 𝐵)) ⊆ On
1817a1i 11 . . . . 5 (𝜑 → ( +no “ ({𝐴} × 𝐵)) ⊆ On)
1912, 18elpwd 4604 . . . 4 (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On)
20 snex 5427 . . . . . . 7 {𝐵} ∈ V
21 xpexg 7724 . . . . . . 7 ((𝐴 ∈ On ∧ {𝐵} ∈ V) → (𝐴 × {𝐵}) ∈ V)
221, 20, 21sylancl 587 . . . . . 6 (𝜑 → (𝐴 × {𝐵}) ∈ V)
23 funimaexg 6626 . . . . . 6 ((Fun +no ∧ (𝐴 × {𝐵}) ∈ V) → ( +no “ (𝐴 × {𝐵})) ∈ V)
247, 22, 23sylancr 588 . . . . 5 (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ V)
25 imassrn 6063 . . . . . . 7 ( +no “ (𝐴 × {𝐵})) ⊆ ran +no
2625, 16sstri 3989 . . . . . 6 ( +no “ (𝐴 × {𝐵})) ⊆ On
2726a1i 11 . . . . 5 (𝜑 → ( +no “ (𝐴 × {𝐵})) ⊆ On)
2824, 27elpwd 4604 . . . 4 (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On)
29 pwuncl 7744 . . . 4 ((( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On ∧ ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On) → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
3019, 28, 29syl2anc 585 . . 3 (𝜑 → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
31 naddunif.3 . . . . . . . . . 10 (𝜑𝐴 = {𝑥 ∈ On ∣ 𝑋𝑥})
3231, 1eqeltrrd 2835 . . . . . . . . 9 (𝜑 {𝑥 ∈ On ∣ 𝑋𝑥} ∈ On)
33 onintrab2 7772 . . . . . . . . 9 (∃𝑥 ∈ On 𝑋𝑥 {𝑥 ∈ On ∣ 𝑋𝑥} ∈ On)
3432, 33sylibr 233 . . . . . . . 8 (𝜑 → ∃𝑥 ∈ On 𝑋𝑥)
35 vex 3479 . . . . . . . . . 10 𝑥 ∈ V
3635ssex 5317 . . . . . . . . 9 (𝑋𝑥𝑋 ∈ V)
3736rexlimivw 3152 . . . . . . . 8 (∃𝑥 ∈ On 𝑋𝑥𝑋 ∈ V)
3834, 37syl 17 . . . . . . 7 (𝜑𝑋 ∈ V)
39 xpexg 7724 . . . . . . 7 ((𝑋 ∈ V ∧ {𝐵} ∈ V) → (𝑋 × {𝐵}) ∈ V)
4038, 20, 39sylancl 587 . . . . . 6 (𝜑 → (𝑋 × {𝐵}) ∈ V)
41 funimaexg 6626 . . . . . 6 ((Fun +no ∧ (𝑋 × {𝐵}) ∈ V) → ( +no “ (𝑋 × {𝐵})) ∈ V)
427, 40, 41sylancr 588 . . . . 5 (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ V)
43 imassrn 6063 . . . . . . 7 ( +no “ (𝑋 × {𝐵})) ⊆ ran +no
4443, 16sstri 3989 . . . . . 6 ( +no “ (𝑋 × {𝐵})) ⊆ On
4544a1i 11 . . . . 5 (𝜑 → ( +no “ (𝑋 × {𝐵})) ⊆ On)
4642, 45elpwd 4604 . . . 4 (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On)
47 naddunif.4 . . . . . . . . . 10 (𝜑𝐵 = {𝑦 ∈ On ∣ 𝑌𝑦})
4847, 2eqeltrrd 2835 . . . . . . . . 9 (𝜑 {𝑦 ∈ On ∣ 𝑌𝑦} ∈ On)
49 onintrab2 7772 . . . . . . . . 9 (∃𝑦 ∈ On 𝑌𝑦 {𝑦 ∈ On ∣ 𝑌𝑦} ∈ On)
5048, 49sylibr 233 . . . . . . . 8 (𝜑 → ∃𝑦 ∈ On 𝑌𝑦)
51 vex 3479 . . . . . . . . . 10 𝑦 ∈ V
5251ssex 5317 . . . . . . . . 9 (𝑌𝑦𝑌 ∈ V)
5352rexlimivw 3152 . . . . . . . 8 (∃𝑦 ∈ On 𝑌𝑦𝑌 ∈ V)
5450, 53syl 17 . . . . . . 7 (𝜑𝑌 ∈ V)
55 xpexg 7724 . . . . . . 7 (({𝐴} ∈ V ∧ 𝑌 ∈ V) → ({𝐴} × 𝑌) ∈ V)
568, 54, 55sylancr 588 . . . . . 6 (𝜑 → ({𝐴} × 𝑌) ∈ V)
57 funimaexg 6626 . . . . . 6 ((Fun +no ∧ ({𝐴} × 𝑌) ∈ V) → ( +no “ ({𝐴} × 𝑌)) ∈ V)
587, 56, 57sylancr 588 . . . . 5 (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ V)
59 imassrn 6063 . . . . . . 7 ( +no “ ({𝐴} × 𝑌)) ⊆ ran +no
6059, 16sstri 3989 . . . . . 6 ( +no “ ({𝐴} × 𝑌)) ⊆ On
6160a1i 11 . . . . 5 (𝜑 → ( +no “ ({𝐴} × 𝑌)) ⊆ On)
6258, 61elpwd 4604 . . . 4 (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On)
63 pwuncl 7744 . . . 4 ((( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On ∧ ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On) → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
6446, 62, 63syl2anc 585 . . 3 (𝜑 → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
652, 47cofonr 8661 . . . . . . . . 9 (𝜑 → ∀𝑞𝐵𝑠𝑌 𝑞𝑠)
66 onss 7759 . . . . . . . . . . . . . . 15 (𝐵 ∈ On → 𝐵 ⊆ On)
672, 66syl 17 . . . . . . . . . . . . . 14 (𝜑𝐵 ⊆ On)
6867sselda 3980 . . . . . . . . . . . . 13 ((𝜑𝑞𝐵) → 𝑞 ∈ On)
6968adantr 482 . . . . . . . . . . . 12 (((𝜑𝑞𝐵) ∧ 𝑠𝑌) → 𝑞 ∈ On)
70 onss 7759 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ On → 𝑦 ⊆ On)
7170adantl 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ On) → 𝑦 ⊆ On)
72 sstr 3988 . . . . . . . . . . . . . . . . . 18 ((𝑌𝑦𝑦 ⊆ On) → 𝑌 ⊆ On)
7372expcom 415 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → (𝑌𝑦𝑌 ⊆ On))
7471, 73syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ On) → (𝑌𝑦𝑌 ⊆ On))
7574rexlimdva 3156 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑦 ∈ On 𝑌𝑦𝑌 ⊆ On))
7650, 75mpd 15 . . . . . . . . . . . . . 14 (𝜑𝑌 ⊆ On)
7776adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑞𝐵) → 𝑌 ⊆ On)
7877sselda 3980 . . . . . . . . . . . 12 (((𝜑𝑞𝐵) ∧ 𝑠𝑌) → 𝑠 ∈ On)
791ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑞𝐵) ∧ 𝑠𝑌) → 𝐴 ∈ On)
80 naddss2 8677 . . . . . . . . . . . 12 ((𝑞 ∈ On ∧ 𝑠 ∈ On ∧ 𝐴 ∈ On) → (𝑞𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
8169, 78, 79, 80syl3anc 1372 . . . . . . . . . . 11 (((𝜑𝑞𝐵) ∧ 𝑠𝑌) → (𝑞𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
8281rexbidva 3177 . . . . . . . . . 10 ((𝜑𝑞𝐵) → (∃𝑠𝑌 𝑞𝑠 ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
8382ralbidva 3176 . . . . . . . . 9 (𝜑 → (∀𝑞𝐵𝑠𝑌 𝑞𝑠 ↔ ∀𝑞𝐵𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
8465, 83mpbid 231 . . . . . . . 8 (𝜑 → ∀𝑞𝐵𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠))
851snssd 4808 . . . . . . . . . . . 12 (𝜑 → {𝐴} ⊆ On)
86 xpss12 5687 . . . . . . . . . . . 12 (({𝐴} ⊆ On ∧ 𝑌 ⊆ On) → ({𝐴} × 𝑌) ⊆ (On × On))
8785, 76, 86syl2anc 585 . . . . . . . . . . 11 (𝜑 → ({𝐴} × 𝑌) ⊆ (On × On))
88 sseq2 4006 . . . . . . . . . . . 12 (𝑑 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
8988imaeqexov 7632 . . . . . . . . . . 11 (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
905, 87, 89sylancr 588 . . . . . . . . . 10 (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
91 oveq1 7403 . . . . . . . . . . . . . 14 (𝑟 = 𝐴 → (𝑟 +no 𝑠) = (𝐴 +no 𝑠))
9291sseq2d 4012 . . . . . . . . . . . . 13 (𝑟 = 𝐴 → ((𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9392rexbidv 3179 . . . . . . . . . . . 12 (𝑟 = 𝐴 → (∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9493rexsng 4674 . . . . . . . . . . 11 (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
951, 94syl 17 . . . . . . . . . 10 (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9690, 95bitrd 279 . . . . . . . . 9 (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9796ralbidv 3178 . . . . . . . 8 (𝜑 → (∀𝑞𝐵𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞𝐵𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9884, 97mpbird 257 . . . . . . 7 (𝜑 → ∀𝑞𝐵𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑)
99 olc 867 . . . . . . . 8 (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
10099ralimi 3084 . . . . . . 7 (∀𝑞𝐵𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → ∀𝑞𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
10198, 100syl 17 . . . . . 6 (𝜑 → ∀𝑞𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
102 rexun 4188 . . . . . . 7 (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
103102ralbii 3094 . . . . . 6 (∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
104101, 103sylibr 233 . . . . 5 (𝜑 → ∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑)
105 xpss12 5687 . . . . . . . 8 (({𝐴} ⊆ On ∧ 𝐵 ⊆ On) → ({𝐴} × 𝐵) ⊆ (On × On))
10685, 67, 105syl2anc 585 . . . . . . 7 (𝜑 → ({𝐴} × 𝐵) ⊆ (On × On))
107 sseq1 4005 . . . . . . . . 9 (𝑐 = (𝑝 +no 𝑞) → (𝑐𝑑 ↔ (𝑝 +no 𝑞) ⊆ 𝑑))
108107rexbidv 3179 . . . . . . . 8 (𝑐 = (𝑝 +no 𝑞) → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
109108imaeqalov 7633 . . . . . . 7 (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
1105, 106, 109sylancr 588 . . . . . 6 (𝜑 → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
111 oveq1 7403 . . . . . . . . . . 11 (𝑝 = 𝐴 → (𝑝 +no 𝑞) = (𝐴 +no 𝑞))
112111sseq1d 4011 . . . . . . . . . 10 (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ 𝑑))
113112rexbidv 3179 . . . . . . . . 9 (𝑝 = 𝐴 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
114113ralbidv 3178 . . . . . . . 8 (𝑝 = 𝐴 → (∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
115114ralsng 4673 . . . . . . 7 (𝐴 ∈ On → (∀𝑝 ∈ {𝐴}∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
1161, 115syl 17 . . . . . 6 (𝜑 → (∀𝑝 ∈ {𝐴}∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
117110, 116bitrd 279 . . . . 5 (𝜑 → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
118104, 117mpbird 257 . . . 4 (𝜑 → ∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑)
1191, 31cofonr 8661 . . . . . . . . . 10 (𝜑 → ∀𝑝𝐴𝑟𝑋 𝑝𝑟)
120 onss 7759 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → 𝐴 ⊆ On)
1211, 120syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐴 ⊆ On)
122121sselda 3980 . . . . . . . . . . . . . 14 ((𝜑𝑝𝐴) → 𝑝 ∈ On)
123122adantr 482 . . . . . . . . . . . . 13 (((𝜑𝑝𝐴) ∧ 𝑟𝑋) → 𝑝 ∈ On)
124 ssintub 4966 . . . . . . . . . . . . . . . 16 𝑋 {𝑥 ∈ On ∣ 𝑋𝑥}
12531, 121eqsstrrd 4019 . . . . . . . . . . . . . . . 16 (𝜑 {𝑥 ∈ On ∣ 𝑋𝑥} ⊆ On)
126124, 125sstrid 3991 . . . . . . . . . . . . . . 15 (𝜑𝑋 ⊆ On)
127126adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑝𝐴) → 𝑋 ⊆ On)
128127sselda 3980 . . . . . . . . . . . . 13 (((𝜑𝑝𝐴) ∧ 𝑟𝑋) → 𝑟 ∈ On)
1292ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑝𝐴) ∧ 𝑟𝑋) → 𝐵 ∈ On)
130 naddss1 8676 . . . . . . . . . . . . 13 ((𝑝 ∈ On ∧ 𝑟 ∈ On ∧ 𝐵 ∈ On) → (𝑝𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
131123, 128, 129, 130syl3anc 1372 . . . . . . . . . . . 12 (((𝜑𝑝𝐴) ∧ 𝑟𝑋) → (𝑝𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
132131rexbidva 3177 . . . . . . . . . . 11 ((𝜑𝑝𝐴) → (∃𝑟𝑋 𝑝𝑟 ↔ ∃𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
133132ralbidva 3176 . . . . . . . . . 10 (𝜑 → (∀𝑝𝐴𝑟𝑋 𝑝𝑟 ↔ ∀𝑝𝐴𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
134119, 133mpbid 231 . . . . . . . . 9 (𝜑 → ∀𝑝𝐴𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
1352snssd 4808 . . . . . . . . . . . . 13 (𝜑 → {𝐵} ⊆ On)
136 xpss12 5687 . . . . . . . . . . . . 13 ((𝑋 ⊆ On ∧ {𝐵} ⊆ On) → (𝑋 × {𝐵}) ⊆ (On × On))
137126, 135, 136syl2anc 585 . . . . . . . . . . . 12 (𝜑 → (𝑋 × {𝐵}) ⊆ (On × On))
138 sseq2 4006 . . . . . . . . . . . . 13 (𝑑 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
139138imaeqexov 7632 . . . . . . . . . . . 12 (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟𝑋𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
1405, 137, 139sylancr 588 . . . . . . . . . . 11 (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟𝑋𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
141 oveq2 7404 . . . . . . . . . . . . . . 15 (𝑠 = 𝐵 → (𝑟 +no 𝑠) = (𝑟 +no 𝐵))
142141sseq2d 4012 . . . . . . . . . . . . . 14 (𝑠 = 𝐵 → ((𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
143142rexsng 4674 . . . . . . . . . . . . 13 (𝐵 ∈ On → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
1442, 143syl 17 . . . . . . . . . . . 12 (𝜑 → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
145144rexbidv 3179 . . . . . . . . . . 11 (𝜑 → (∃𝑟𝑋𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
146140, 145bitrd 279 . . . . . . . . . 10 (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
147146ralbidv 3178 . . . . . . . . 9 (𝜑 → (∀𝑝𝐴𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝𝐴𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
148134, 147mpbird 257 . . . . . . . 8 (𝜑 → ∀𝑝𝐴𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑)
149 orc 866 . . . . . . . . 9 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
150149ralimi 3084 . . . . . . . 8 (∀𝑝𝐴𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → ∀𝑝𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
151148, 150syl 17 . . . . . . 7 (𝜑 → ∀𝑝𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
152 rexun 4188 . . . . . . . 8 (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
153152ralbii 3094 . . . . . . 7 (∀𝑝𝐴𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
154151, 153sylibr 233 . . . . . 6 (𝜑 → ∀𝑝𝐴𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑)
155 oveq2 7404 . . . . . . . . . . 11 (𝑞 = 𝐵 → (𝑝 +no 𝑞) = (𝑝 +no 𝐵))
156155sseq1d 4011 . . . . . . . . . 10 (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ 𝑑))
157156rexbidv 3179 . . . . . . . . 9 (𝑞 = 𝐵 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
158157ralsng 4673 . . . . . . . 8 (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
1592, 158syl 17 . . . . . . 7 (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
160159ralbidv 3178 . . . . . 6 (𝜑 → (∀𝑝𝐴𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑝𝐴𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
161154, 160mpbird 257 . . . . 5 (𝜑 → ∀𝑝𝐴𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑)
162 xpss12 5687 . . . . . . 7 ((𝐴 ⊆ On ∧ {𝐵} ⊆ On) → (𝐴 × {𝐵}) ⊆ (On × On))
163121, 135, 162syl2anc 585 . . . . . 6 (𝜑 → (𝐴 × {𝐵}) ⊆ (On × On))
164108imaeqalov 7633 . . . . . 6 (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑝𝐴𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
1655, 163, 164sylancr 588 . . . . 5 (𝜑 → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑝𝐴𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
166161, 165mpbird 257 . . . 4 (𝜑 → ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑)
167 ralunb 4189 . . . 4 (∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ∧ ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑))
168118, 166, 167sylanbrc 584 . . 3 (𝜑 → ∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑)
169124, 31sseqtrrid 4033 . . . . . . . . . . . 12 (𝜑𝑋𝐴)
170169sselda 3980 . . . . . . . . . . 11 ((𝜑𝑝𝑋) → 𝑝𝐴)
171 ssid 4002 . . . . . . . . . . 11 𝑝𝑝
172 sseq2 4006 . . . . . . . . . . . 12 (𝑟 = 𝑝 → (𝑝𝑟𝑝𝑝))
173172rspcev 3611 . . . . . . . . . . 11 ((𝑝𝐴𝑝𝑝) → ∃𝑟𝐴 𝑝𝑟)
174170, 171, 173sylancl 587 . . . . . . . . . 10 ((𝜑𝑝𝑋) → ∃𝑟𝐴 𝑝𝑟)
175174ralrimiva 3147 . . . . . . . . 9 (𝜑 → ∀𝑝𝑋𝑟𝐴 𝑝𝑟)
176126sselda 3980 . . . . . . . . . . . . 13 ((𝜑𝑝𝑋) → 𝑝 ∈ On)
177176adantr 482 . . . . . . . . . . . 12 (((𝜑𝑝𝑋) ∧ 𝑟𝐴) → 𝑝 ∈ On)
178121adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑝𝑋) → 𝐴 ⊆ On)
179178sselda 3980 . . . . . . . . . . . 12 (((𝜑𝑝𝑋) ∧ 𝑟𝐴) → 𝑟 ∈ On)
1802ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑝𝑋) ∧ 𝑟𝐴) → 𝐵 ∈ On)
181177, 179, 180, 130syl3anc 1372 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑟𝐴) → (𝑝𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
182181rexbidva 3177 . . . . . . . . . 10 ((𝜑𝑝𝑋) → (∃𝑟𝐴 𝑝𝑟 ↔ ∃𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
183182ralbidva 3176 . . . . . . . . 9 (𝜑 → (∀𝑝𝑋𝑟𝐴 𝑝𝑟 ↔ ∀𝑝𝑋𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
184175, 183mpbid 231 . . . . . . . 8 (𝜑 → ∀𝑝𝑋𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
185 sseq2 4006 . . . . . . . . . . . 12 (𝑏 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
186185imaeqexov 7632 . . . . . . . . . . 11 (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟𝐴𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
1875, 163, 186sylancr 588 . . . . . . . . . 10 (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟𝐴𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
188144rexbidv 3179 . . . . . . . . . 10 (𝜑 → (∃𝑟𝐴𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
189187, 188bitrd 279 . . . . . . . . 9 (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
190189ralbidv 3178 . . . . . . . 8 (𝜑 → (∀𝑝𝑋𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∀𝑝𝑋𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
191184, 190mpbird 257 . . . . . . 7 (𝜑 → ∀𝑝𝑋𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)
192 olc 867 . . . . . . . 8 (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
193192ralimi 3084 . . . . . . 7 (∀𝑝𝑋𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → ∀𝑝𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
194191, 193syl 17 . . . . . 6 (𝜑 → ∀𝑝𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
195155sseq1d 4011 . . . . . . . . . . . 12 (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ 𝑏))
196195rexbidv 3179 . . . . . . . . . . 11 (𝑞 = 𝐵 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
197196ralsng 4673 . . . . . . . . . 10 (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
1982, 197syl 17 . . . . . . . . 9 (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
199198adantr 482 . . . . . . . 8 ((𝜑𝑝𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
200 rexun 4188 . . . . . . . 8 (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
201199, 200bitrdi 287 . . . . . . 7 ((𝜑𝑝𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
202201ralbidva 3176 . . . . . 6 (𝜑 → (∀𝑝𝑋𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑝𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
203194, 202mpbird 257 . . . . 5 (𝜑 → ∀𝑝𝑋𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏)
204 sseq1 4005 . . . . . . . 8 (𝑎 = (𝑝 +no 𝑞) → (𝑎𝑏 ↔ (𝑝 +no 𝑞) ⊆ 𝑏))
205204rexbidv 3179 . . . . . . 7 (𝑎 = (𝑝 +no 𝑞) → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
206205imaeqalov 7633 . . . . . 6 (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∀𝑝𝑋𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
2075, 137, 206sylancr 588 . . . . 5 (𝜑 → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∀𝑝𝑋𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
208203, 207mpbird 257 . . . 4 (𝜑 → ∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏)
209 ssintub 4966 . . . . . . . . . . . . 13 𝑌 {𝑦 ∈ On ∣ 𝑌𝑦}
210209, 47sseqtrrid 4033 . . . . . . . . . . . 12 (𝜑𝑌𝐵)
211210sselda 3980 . . . . . . . . . . 11 ((𝜑𝑞𝑌) → 𝑞𝐵)
212 ssid 4002 . . . . . . . . . . 11 𝑞𝑞
213 sseq2 4006 . . . . . . . . . . . 12 (𝑠 = 𝑞 → (𝑞𝑠𝑞𝑞))
214213rspcev 3611 . . . . . . . . . . 11 ((𝑞𝐵𝑞𝑞) → ∃𝑠𝐵 𝑞𝑠)
215211, 212, 214sylancl 587 . . . . . . . . . 10 ((𝜑𝑞𝑌) → ∃𝑠𝐵 𝑞𝑠)
216215ralrimiva 3147 . . . . . . . . 9 (𝜑 → ∀𝑞𝑌𝑠𝐵 𝑞𝑠)
21792rexbidv 3179 . . . . . . . . . . . . . 14 (𝑟 = 𝐴 → (∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
218217rexsng 4674 . . . . . . . . . . . . 13 (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
2191, 218syl 17 . . . . . . . . . . . 12 (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
220219adantr 482 . . . . . . . . . . 11 ((𝜑𝑞𝑌) → (∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
221 sseq2 4006 . . . . . . . . . . . . . 14 (𝑏 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
222221imaeqexov 7632 . . . . . . . . . . . . 13 (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
2235, 106, 222sylancr 588 . . . . . . . . . . . 12 (𝜑 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
224223adantr 482 . . . . . . . . . . 11 ((𝜑𝑞𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
22576sselda 3980 . . . . . . . . . . . . . 14 ((𝜑𝑞𝑌) → 𝑞 ∈ On)
226225adantr 482 . . . . . . . . . . . . 13 (((𝜑𝑞𝑌) ∧ 𝑠𝐵) → 𝑞 ∈ On)
22767adantr 482 . . . . . . . . . . . . . 14 ((𝜑𝑞𝑌) → 𝐵 ⊆ On)
228227sselda 3980 . . . . . . . . . . . . 13 (((𝜑𝑞𝑌) ∧ 𝑠𝐵) → 𝑠 ∈ On)
2291ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑞𝑌) ∧ 𝑠𝐵) → 𝐴 ∈ On)
230226, 228, 229, 80syl3anc 1372 . . . . . . . . . . . 12 (((𝜑𝑞𝑌) ∧ 𝑠𝐵) → (𝑞𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
231230rexbidva 3177 . . . . . . . . . . 11 ((𝜑𝑞𝑌) → (∃𝑠𝐵 𝑞𝑠 ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
232220, 224, 2313bitr4d 311 . . . . . . . . . 10 ((𝜑𝑞𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑠𝐵 𝑞𝑠))
233232ralbidva 3176 . . . . . . . . 9 (𝜑 → (∀𝑞𝑌𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞𝑌𝑠𝐵 𝑞𝑠))
234216, 233mpbird 257 . . . . . . . 8 (𝜑 → ∀𝑞𝑌𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏)
235 orc 866 . . . . . . . . 9 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
236235ralimi 3084 . . . . . . . 8 (∀𝑞𝑌𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → ∀𝑞𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
237234, 236syl 17 . . . . . . 7 (𝜑 → ∀𝑞𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
238 rexun 4188 . . . . . . . 8 (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
239238ralbii 3094 . . . . . . 7 (∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
240237, 239sylibr 233 . . . . . 6 (𝜑 → ∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏)
241111sseq1d 4011 . . . . . . . . . 10 (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ 𝑏))
242241rexbidv 3179 . . . . . . . . 9 (𝑝 = 𝐴 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
243242ralbidv 3178 . . . . . . . 8 (𝑝 = 𝐴 → (∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
244243ralsng 4673 . . . . . . 7 (𝐴 ∈ On → (∀𝑝 ∈ {𝐴}∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
2451, 244syl 17 . . . . . 6 (𝜑 → (∀𝑝 ∈ {𝐴}∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
246240, 245mpbird 257 . . . . 5 (𝜑 → ∀𝑝 ∈ {𝐴}∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏)
247205imaeqalov 7633 . . . . . 6 (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
2485, 87, 247sylancr 588 . . . . 5 (𝜑 → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
249246, 248mpbird 257 . . . 4 (𝜑 → ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏)
250 ralunb 4189 . . . 4 (∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ∧ ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏))
251208, 249, 250sylanbrc 584 . . 3 (𝜑 → ∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏)
25230, 64, 168, 251cofon2 8660 . 2 (𝜑 {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤} = {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
2534, 252eqtrd 2773 1 (𝜑 → (𝐴 +no 𝐵) = {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wcel 2107  wral 3062  wrex 3071  {crab 3433  Vcvv 3475  cun 3944  wss 3946  𝒫 cpw 4598  {csn 4624   cint 4946   × cxp 5670  ran crn 5673  cima 5675  Oncon0 6356  Fun wfun 6529   Fn wfn 6530  wf 6531  (class class class)co 7396   +no cnadd 8652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-int 4947  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7962  df-2nd 7963  df-frecs 8253  df-nadd 8653
This theorem is referenced by:  naddasslem1  8681  naddasslem2  8682
  Copyright terms: Public domain W3C validator