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

Theorem naddunif 8729
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 8716 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
41, 2, 3syl2anc 584 . 2 (𝜑 → (𝐴 +no 𝐵) = {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
5 naddfn 8711 . . . . . . 7 +no Fn (On × On)
6 fnfun 6668 . . . . . . 7 ( +no Fn (On × On) → Fun +no )
75, 6ax-mp 5 . . . . . 6 Fun +no
8 snex 5441 . . . . . . 7 {𝐴} ∈ V
9 xpexg 7768 . . . . . . 7 (({𝐴} ∈ V ∧ 𝐵 ∈ On) → ({𝐴} × 𝐵) ∈ V)
108, 2, 9sylancr 587 . . . . . 6 (𝜑 → ({𝐴} × 𝐵) ∈ V)
11 funimaexg 6653 . . . . . 6 ((Fun +no ∧ ({𝐴} × 𝐵) ∈ V) → ( +no “ ({𝐴} × 𝐵)) ∈ V)
127, 10, 11sylancr 587 . . . . 5 (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ V)
13 imassrn 6090 . . . . . . 7 ( +no “ ({𝐴} × 𝐵)) ⊆ ran +no
14 naddf 8717 . . . . . . . 8 +no :(On × On)⟶On
15 frn 6743 . . . . . . . 8 ( +no :(On × On)⟶On → ran +no ⊆ On)
1614, 15ax-mp 5 . . . . . . 7 ran +no ⊆ On
1713, 16sstri 4004 . . . . . 6 ( +no “ ({𝐴} × 𝐵)) ⊆ On
1817a1i 11 . . . . 5 (𝜑 → ( +no “ ({𝐴} × 𝐵)) ⊆ On)
1912, 18elpwd 4610 . . . 4 (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On)
20 snex 5441 . . . . . . 7 {𝐵} ∈ V
21 xpexg 7768 . . . . . . 7 ((𝐴 ∈ On ∧ {𝐵} ∈ V) → (𝐴 × {𝐵}) ∈ V)
221, 20, 21sylancl 586 . . . . . 6 (𝜑 → (𝐴 × {𝐵}) ∈ V)
23 funimaexg 6653 . . . . . 6 ((Fun +no ∧ (𝐴 × {𝐵}) ∈ V) → ( +no “ (𝐴 × {𝐵})) ∈ V)
247, 22, 23sylancr 587 . . . . 5 (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ V)
25 imassrn 6090 . . . . . . 7 ( +no “ (𝐴 × {𝐵})) ⊆ ran +no
2625, 16sstri 4004 . . . . . 6 ( +no “ (𝐴 × {𝐵})) ⊆ On
2726a1i 11 . . . . 5 (𝜑 → ( +no “ (𝐴 × {𝐵})) ⊆ On)
2824, 27elpwd 4610 . . . 4 (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On)
29 pwuncl 7788 . . . 4 ((( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On ∧ ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On) → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
3019, 28, 29syl2anc 584 . . 3 (𝜑 → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
31 naddunif.3 . . . . . . . . . 10 (𝜑𝐴 = {𝑥 ∈ On ∣ 𝑋𝑥})
3231, 1eqeltrrd 2839 . . . . . . . . 9 (𝜑 {𝑥 ∈ On ∣ 𝑋𝑥} ∈ On)
33 onintrab2 7816 . . . . . . . . 9 (∃𝑥 ∈ On 𝑋𝑥 {𝑥 ∈ On ∣ 𝑋𝑥} ∈ On)
3432, 33sylibr 234 . . . . . . . 8 (𝜑 → ∃𝑥 ∈ On 𝑋𝑥)
35 vex 3481 . . . . . . . . . 10 𝑥 ∈ V
3635ssex 5326 . . . . . . . . 9 (𝑋𝑥𝑋 ∈ V)
3736rexlimivw 3148 . . . . . . . 8 (∃𝑥 ∈ On 𝑋𝑥𝑋 ∈ V)
3834, 37syl 17 . . . . . . 7 (𝜑𝑋 ∈ V)
39 xpexg 7768 . . . . . . 7 ((𝑋 ∈ V ∧ {𝐵} ∈ V) → (𝑋 × {𝐵}) ∈ V)
4038, 20, 39sylancl 586 . . . . . 6 (𝜑 → (𝑋 × {𝐵}) ∈ V)
41 funimaexg 6653 . . . . . 6 ((Fun +no ∧ (𝑋 × {𝐵}) ∈ V) → ( +no “ (𝑋 × {𝐵})) ∈ V)
427, 40, 41sylancr 587 . . . . 5 (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ V)
43 imassrn 6090 . . . . . . 7 ( +no “ (𝑋 × {𝐵})) ⊆ ran +no
4443, 16sstri 4004 . . . . . 6 ( +no “ (𝑋 × {𝐵})) ⊆ On
4544a1i 11 . . . . 5 (𝜑 → ( +no “ (𝑋 × {𝐵})) ⊆ On)
4642, 45elpwd 4610 . . . 4 (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On)
47 naddunif.4 . . . . . . . . . 10 (𝜑𝐵 = {𝑦 ∈ On ∣ 𝑌𝑦})
4847, 2eqeltrrd 2839 . . . . . . . . 9 (𝜑 {𝑦 ∈ On ∣ 𝑌𝑦} ∈ On)
49 onintrab2 7816 . . . . . . . . 9 (∃𝑦 ∈ On 𝑌𝑦 {𝑦 ∈ On ∣ 𝑌𝑦} ∈ On)
5048, 49sylibr 234 . . . . . . . 8 (𝜑 → ∃𝑦 ∈ On 𝑌𝑦)
51 vex 3481 . . . . . . . . . 10 𝑦 ∈ V
5251ssex 5326 . . . . . . . . 9 (𝑌𝑦𝑌 ∈ V)
5352rexlimivw 3148 . . . . . . . 8 (∃𝑦 ∈ On 𝑌𝑦𝑌 ∈ V)
5450, 53syl 17 . . . . . . 7 (𝜑𝑌 ∈ V)
55 xpexg 7768 . . . . . . 7 (({𝐴} ∈ V ∧ 𝑌 ∈ V) → ({𝐴} × 𝑌) ∈ V)
568, 54, 55sylancr 587 . . . . . 6 (𝜑 → ({𝐴} × 𝑌) ∈ V)
57 funimaexg 6653 . . . . . 6 ((Fun +no ∧ ({𝐴} × 𝑌) ∈ V) → ( +no “ ({𝐴} × 𝑌)) ∈ V)
587, 56, 57sylancr 587 . . . . 5 (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ V)
59 imassrn 6090 . . . . . . 7 ( +no “ ({𝐴} × 𝑌)) ⊆ ran +no
6059, 16sstri 4004 . . . . . 6 ( +no “ ({𝐴} × 𝑌)) ⊆ On
6160a1i 11 . . . . 5 (𝜑 → ( +no “ ({𝐴} × 𝑌)) ⊆ On)
6258, 61elpwd 4610 . . . 4 (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On)
63 pwuncl 7788 . . . 4 ((( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On ∧ ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On) → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
6446, 62, 63syl2anc 584 . . 3 (𝜑 → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
652, 47cofonr 8710 . . . . . . . . 9 (𝜑 → ∀𝑞𝐵𝑠𝑌 𝑞𝑠)
66 onss 7803 . . . . . . . . . . . . . . 15 (𝐵 ∈ On → 𝐵 ⊆ On)
672, 66syl 17 . . . . . . . . . . . . . 14 (𝜑𝐵 ⊆ On)
6867sselda 3994 . . . . . . . . . . . . 13 ((𝜑𝑞𝐵) → 𝑞 ∈ On)
6968adantr 480 . . . . . . . . . . . 12 (((𝜑𝑞𝐵) ∧ 𝑠𝑌) → 𝑞 ∈ On)
70 onss 7803 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ On → 𝑦 ⊆ On)
7170adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ On) → 𝑦 ⊆ On)
72 sstr 4003 . . . . . . . . . . . . . . . . . 18 ((𝑌𝑦𝑦 ⊆ On) → 𝑌 ⊆ On)
7372expcom 413 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → (𝑌𝑦𝑌 ⊆ On))
7471, 73syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ On) → (𝑌𝑦𝑌 ⊆ On))
7574rexlimdva 3152 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑦 ∈ On 𝑌𝑦𝑌 ⊆ On))
7650, 75mpd 15 . . . . . . . . . . . . . 14 (𝜑𝑌 ⊆ On)
7776adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑞𝐵) → 𝑌 ⊆ On)
7877sselda 3994 . . . . . . . . . . . 12 (((𝜑𝑞𝐵) ∧ 𝑠𝑌) → 𝑠 ∈ On)
791ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑞𝐵) ∧ 𝑠𝑌) → 𝐴 ∈ On)
80 naddss2 8726 . . . . . . . . . . . 12 ((𝑞 ∈ On ∧ 𝑠 ∈ On ∧ 𝐴 ∈ On) → (𝑞𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
8169, 78, 79, 80syl3anc 1370 . . . . . . . . . . 11 (((𝜑𝑞𝐵) ∧ 𝑠𝑌) → (𝑞𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
8281rexbidva 3174 . . . . . . . . . 10 ((𝜑𝑞𝐵) → (∃𝑠𝑌 𝑞𝑠 ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
8382ralbidva 3173 . . . . . . . . 9 (𝜑 → (∀𝑞𝐵𝑠𝑌 𝑞𝑠 ↔ ∀𝑞𝐵𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
8465, 83mpbid 232 . . . . . . . 8 (𝜑 → ∀𝑞𝐵𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠))
851snssd 4813 . . . . . . . . . . . 12 (𝜑 → {𝐴} ⊆ On)
86 xpss12 5703 . . . . . . . . . . . 12 (({𝐴} ⊆ On ∧ 𝑌 ⊆ On) → ({𝐴} × 𝑌) ⊆ (On × On))
8785, 76, 86syl2anc 584 . . . . . . . . . . 11 (𝜑 → ({𝐴} × 𝑌) ⊆ (On × On))
88 sseq2 4021 . . . . . . . . . . . 12 (𝑑 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
8988imaeqexov 7670 . . . . . . . . . . 11 (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
905, 87, 89sylancr 587 . . . . . . . . . 10 (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
91 oveq1 7437 . . . . . . . . . . . . . 14 (𝑟 = 𝐴 → (𝑟 +no 𝑠) = (𝐴 +no 𝑠))
9291sseq2d 4027 . . . . . . . . . . . . 13 (𝑟 = 𝐴 → ((𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9392rexbidv 3176 . . . . . . . . . . . 12 (𝑟 = 𝐴 → (∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9493rexsng 4680 . . . . . . . . . . 11 (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
951, 94syl 17 . . . . . . . . . 10 (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9690, 95bitrd 279 . . . . . . . . 9 (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9796ralbidv 3175 . . . . . . . 8 (𝜑 → (∀𝑞𝐵𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞𝐵𝑠𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
9884, 97mpbird 257 . . . . . . 7 (𝜑 → ∀𝑞𝐵𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑)
99 olc 868 . . . . . . . 8 (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
10099ralimi 3080 . . . . . . 7 (∀𝑞𝐵𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → ∀𝑞𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
10198, 100syl 17 . . . . . 6 (𝜑 → ∀𝑞𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
102 rexun 4205 . . . . . . 7 (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
103102ralbii 3090 . . . . . 6 (∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
104101, 103sylibr 234 . . . . 5 (𝜑 → ∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑)
105 xpss12 5703 . . . . . . . 8 (({𝐴} ⊆ On ∧ 𝐵 ⊆ On) → ({𝐴} × 𝐵) ⊆ (On × On))
10685, 67, 105syl2anc 584 . . . . . . 7 (𝜑 → ({𝐴} × 𝐵) ⊆ (On × On))
107 sseq1 4020 . . . . . . . . 9 (𝑐 = (𝑝 +no 𝑞) → (𝑐𝑑 ↔ (𝑝 +no 𝑞) ⊆ 𝑑))
108107rexbidv 3176 . . . . . . . 8 (𝑐 = (𝑝 +no 𝑞) → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
109108imaeqalov 7671 . . . . . . 7 (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
1105, 106, 109sylancr 587 . . . . . 6 (𝜑 → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
111 oveq1 7437 . . . . . . . . . . 11 (𝑝 = 𝐴 → (𝑝 +no 𝑞) = (𝐴 +no 𝑞))
112111sseq1d 4026 . . . . . . . . . 10 (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ 𝑑))
113112rexbidv 3176 . . . . . . . . 9 (𝑝 = 𝐴 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
114113ralbidv 3175 . . . . . . . 8 (𝑝 = 𝐴 → (∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞𝐵𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
115114ralsng 4679 . . . . . . 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 8710 . . . . . . . . . 10 (𝜑 → ∀𝑝𝐴𝑟𝑋 𝑝𝑟)
120 onss 7803 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → 𝐴 ⊆ On)
1211, 120syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐴 ⊆ On)
122121sselda 3994 . . . . . . . . . . . . . 14 ((𝜑𝑝𝐴) → 𝑝 ∈ On)
123122adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑝𝐴) ∧ 𝑟𝑋) → 𝑝 ∈ On)
124 ssintub 4970 . . . . . . . . . . . . . . . 16 𝑋 {𝑥 ∈ On ∣ 𝑋𝑥}
12531, 121eqsstrrd 4034 . . . . . . . . . . . . . . . 16 (𝜑 {𝑥 ∈ On ∣ 𝑋𝑥} ⊆ On)
126124, 125sstrid 4006 . . . . . . . . . . . . . . 15 (𝜑𝑋 ⊆ On)
127126adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑝𝐴) → 𝑋 ⊆ On)
128127sselda 3994 . . . . . . . . . . . . 13 (((𝜑𝑝𝐴) ∧ 𝑟𝑋) → 𝑟 ∈ On)
1292ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑝𝐴) ∧ 𝑟𝑋) → 𝐵 ∈ On)
130 naddss1 8725 . . . . . . . . . . . . 13 ((𝑝 ∈ On ∧ 𝑟 ∈ On ∧ 𝐵 ∈ On) → (𝑝𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
131123, 128, 129, 130syl3anc 1370 . . . . . . . . . . . 12 (((𝜑𝑝𝐴) ∧ 𝑟𝑋) → (𝑝𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
132131rexbidva 3174 . . . . . . . . . . 11 ((𝜑𝑝𝐴) → (∃𝑟𝑋 𝑝𝑟 ↔ ∃𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
133132ralbidva 3173 . . . . . . . . . 10 (𝜑 → (∀𝑝𝐴𝑟𝑋 𝑝𝑟 ↔ ∀𝑝𝐴𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
134119, 133mpbid 232 . . . . . . . . 9 (𝜑 → ∀𝑝𝐴𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
1352snssd 4813 . . . . . . . . . . . . 13 (𝜑 → {𝐵} ⊆ On)
136 xpss12 5703 . . . . . . . . . . . . 13 ((𝑋 ⊆ On ∧ {𝐵} ⊆ On) → (𝑋 × {𝐵}) ⊆ (On × On))
137126, 135, 136syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑋 × {𝐵}) ⊆ (On × On))
138 sseq2 4021 . . . . . . . . . . . . 13 (𝑑 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
139138imaeqexov 7670 . . . . . . . . . . . 12 (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟𝑋𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
1405, 137, 139sylancr 587 . . . . . . . . . . 11 (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟𝑋𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
141 oveq2 7438 . . . . . . . . . . . . . . 15 (𝑠 = 𝐵 → (𝑟 +no 𝑠) = (𝑟 +no 𝐵))
142141sseq2d 4027 . . . . . . . . . . . . . 14 (𝑠 = 𝐵 → ((𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
143142rexsng 4680 . . . . . . . . . . . . 13 (𝐵 ∈ On → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
1442, 143syl 17 . . . . . . . . . . . 12 (𝜑 → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
145144rexbidv 3176 . . . . . . . . . . 11 (𝜑 → (∃𝑟𝑋𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
146140, 145bitrd 279 . . . . . . . . . 10 (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
147146ralbidv 3175 . . . . . . . . 9 (𝜑 → (∀𝑝𝐴𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝𝐴𝑟𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
148134, 147mpbird 257 . . . . . . . 8 (𝜑 → ∀𝑝𝐴𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑)
149 orc 867 . . . . . . . . 9 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
150149ralimi 3080 . . . . . . . 8 (∀𝑝𝐴𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → ∀𝑝𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
151148, 150syl 17 . . . . . . 7 (𝜑 → ∀𝑝𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
152 rexun 4205 . . . . . . . 8 (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
153152ralbii 3090 . . . . . . 7 (∀𝑝𝐴𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
154151, 153sylibr 234 . . . . . 6 (𝜑 → ∀𝑝𝐴𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑)
155 oveq2 7438 . . . . . . . . . . 11 (𝑞 = 𝐵 → (𝑝 +no 𝑞) = (𝑝 +no 𝐵))
156155sseq1d 4026 . . . . . . . . . 10 (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ 𝑑))
157156rexbidv 3176 . . . . . . . . 9 (𝑞 = 𝐵 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
158157ralsng 4679 . . . . . . . 8 (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
1592, 158syl 17 . . . . . . 7 (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
160159ralbidv 3175 . . . . . 6 (𝜑 → (∀𝑝𝐴𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑝𝐴𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
161154, 160mpbird 257 . . . . 5 (𝜑 → ∀𝑝𝐴𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑)
162 xpss12 5703 . . . . . . 7 ((𝐴 ⊆ On ∧ {𝐵} ⊆ On) → (𝐴 × {𝐵}) ⊆ (On × On))
163121, 135, 162syl2anc 584 . . . . . 6 (𝜑 → (𝐴 × {𝐵}) ⊆ (On × On))
164108imaeqalov 7671 . . . . . 6 (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑝𝐴𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
1655, 163, 164sylancr 587 . . . . 5 (𝜑 → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ ∀𝑝𝐴𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
166161, 165mpbird 257 . . . 4 (𝜑 → ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑)
167 ralunb 4206 . . . 4 (∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ↔ (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑 ∧ ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑))
168118, 166, 167sylanbrc 583 . . 3 (𝜑 → ∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐𝑑)
169124, 31sseqtrrid 4048 . . . . . . . . . . . 12 (𝜑𝑋𝐴)
170169sselda 3994 . . . . . . . . . . 11 ((𝜑𝑝𝑋) → 𝑝𝐴)
171 ssid 4017 . . . . . . . . . . 11 𝑝𝑝
172 sseq2 4021 . . . . . . . . . . . 12 (𝑟 = 𝑝 → (𝑝𝑟𝑝𝑝))
173172rspcev 3621 . . . . . . . . . . 11 ((𝑝𝐴𝑝𝑝) → ∃𝑟𝐴 𝑝𝑟)
174170, 171, 173sylancl 586 . . . . . . . . . 10 ((𝜑𝑝𝑋) → ∃𝑟𝐴 𝑝𝑟)
175174ralrimiva 3143 . . . . . . . . 9 (𝜑 → ∀𝑝𝑋𝑟𝐴 𝑝𝑟)
176126sselda 3994 . . . . . . . . . . . . 13 ((𝜑𝑝𝑋) → 𝑝 ∈ On)
177176adantr 480 . . . . . . . . . . . 12 (((𝜑𝑝𝑋) ∧ 𝑟𝐴) → 𝑝 ∈ On)
178121adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑝𝑋) → 𝐴 ⊆ On)
179178sselda 3994 . . . . . . . . . . . 12 (((𝜑𝑝𝑋) ∧ 𝑟𝐴) → 𝑟 ∈ On)
1802ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑝𝑋) ∧ 𝑟𝐴) → 𝐵 ∈ On)
181177, 179, 180, 130syl3anc 1370 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑟𝐴) → (𝑝𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
182181rexbidva 3174 . . . . . . . . . 10 ((𝜑𝑝𝑋) → (∃𝑟𝐴 𝑝𝑟 ↔ ∃𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
183182ralbidva 3173 . . . . . . . . 9 (𝜑 → (∀𝑝𝑋𝑟𝐴 𝑝𝑟 ↔ ∀𝑝𝑋𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
184175, 183mpbid 232 . . . . . . . 8 (𝜑 → ∀𝑝𝑋𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
185 sseq2 4021 . . . . . . . . . . . 12 (𝑏 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
186185imaeqexov 7670 . . . . . . . . . . 11 (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟𝐴𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
1875, 163, 186sylancr 587 . . . . . . . . . 10 (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟𝐴𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
188144rexbidv 3176 . . . . . . . . . 10 (𝜑 → (∃𝑟𝐴𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
189187, 188bitrd 279 . . . . . . . . 9 (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
190189ralbidv 3175 . . . . . . . 8 (𝜑 → (∀𝑝𝑋𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∀𝑝𝑋𝑟𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
191184, 190mpbird 257 . . . . . . 7 (𝜑 → ∀𝑝𝑋𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)
192 olc 868 . . . . . . . 8 (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
193192ralimi 3080 . . . . . . 7 (∀𝑝𝑋𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → ∀𝑝𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
194191, 193syl 17 . . . . . 6 (𝜑 → ∀𝑝𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
195155sseq1d 4026 . . . . . . . . . . . 12 (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ 𝑏))
196195rexbidv 3176 . . . . . . . . . . 11 (𝑞 = 𝐵 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
197196ralsng 4679 . . . . . . . . . 10 (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
1982, 197syl 17 . . . . . . . . 9 (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
199198adantr 480 . . . . . . . 8 ((𝜑𝑝𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
200 rexun 4205 . . . . . . . 8 (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
201199, 200bitrdi 287 . . . . . . 7 ((𝜑𝑝𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
202201ralbidva 3173 . . . . . 6 (𝜑 → (∀𝑝𝑋𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑝𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
203194, 202mpbird 257 . . . . 5 (𝜑 → ∀𝑝𝑋𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏)
204 sseq1 4020 . . . . . . . 8 (𝑎 = (𝑝 +no 𝑞) → (𝑎𝑏 ↔ (𝑝 +no 𝑞) ⊆ 𝑏))
205204rexbidv 3176 . . . . . . 7 (𝑎 = (𝑝 +no 𝑞) → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
206205imaeqalov 7671 . . . . . 6 (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∀𝑝𝑋𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
2075, 137, 206sylancr 587 . . . . 5 (𝜑 → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∀𝑝𝑋𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
208203, 207mpbird 257 . . . 4 (𝜑 → ∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏)
209 ssintub 4970 . . . . . . . . . . . . 13 𝑌 {𝑦 ∈ On ∣ 𝑌𝑦}
210209, 47sseqtrrid 4048 . . . . . . . . . . . 12 (𝜑𝑌𝐵)
211210sselda 3994 . . . . . . . . . . 11 ((𝜑𝑞𝑌) → 𝑞𝐵)
212 ssid 4017 . . . . . . . . . . 11 𝑞𝑞
213 sseq2 4021 . . . . . . . . . . . 12 (𝑠 = 𝑞 → (𝑞𝑠𝑞𝑞))
214213rspcev 3621 . . . . . . . . . . 11 ((𝑞𝐵𝑞𝑞) → ∃𝑠𝐵 𝑞𝑠)
215211, 212, 214sylancl 586 . . . . . . . . . 10 ((𝜑𝑞𝑌) → ∃𝑠𝐵 𝑞𝑠)
216215ralrimiva 3143 . . . . . . . . 9 (𝜑 → ∀𝑞𝑌𝑠𝐵 𝑞𝑠)
21792rexbidv 3176 . . . . . . . . . . . . . 14 (𝑟 = 𝐴 → (∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
218217rexsng 4680 . . . . . . . . . . . . 13 (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
2191, 218syl 17 . . . . . . . . . . . 12 (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
220219adantr 480 . . . . . . . . . . 11 ((𝜑𝑞𝑌) → (∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
221 sseq2 4021 . . . . . . . . . . . . . 14 (𝑏 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
222221imaeqexov 7670 . . . . . . . . . . . . 13 (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
2235, 106, 222sylancr 587 . . . . . . . . . . . 12 (𝜑 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
224223adantr 480 . . . . . . . . . . 11 ((𝜑𝑞𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
22576sselda 3994 . . . . . . . . . . . . . 14 ((𝜑𝑞𝑌) → 𝑞 ∈ On)
226225adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑞𝑌) ∧ 𝑠𝐵) → 𝑞 ∈ On)
22767adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑞𝑌) → 𝐵 ⊆ On)
228227sselda 3994 . . . . . . . . . . . . 13 (((𝜑𝑞𝑌) ∧ 𝑠𝐵) → 𝑠 ∈ On)
2291ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑞𝑌) ∧ 𝑠𝐵) → 𝐴 ∈ On)
230226, 228, 229, 80syl3anc 1370 . . . . . . . . . . . 12 (((𝜑𝑞𝑌) ∧ 𝑠𝐵) → (𝑞𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
231230rexbidva 3174 . . . . . . . . . . 11 ((𝜑𝑞𝑌) → (∃𝑠𝐵 𝑞𝑠 ↔ ∃𝑠𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
232220, 224, 2313bitr4d 311 . . . . . . . . . 10 ((𝜑𝑞𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑠𝐵 𝑞𝑠))
233232ralbidva 3173 . . . . . . . . 9 (𝜑 → (∀𝑞𝑌𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞𝑌𝑠𝐵 𝑞𝑠))
234216, 233mpbird 257 . . . . . . . 8 (𝜑 → ∀𝑞𝑌𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏)
235 orc 867 . . . . . . . . 9 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
236235ralimi 3080 . . . . . . . 8 (∀𝑞𝑌𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → ∀𝑞𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
237234, 236syl 17 . . . . . . 7 (𝜑 → ∀𝑞𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
238 rexun 4205 . . . . . . . 8 (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
239238ralbii 3090 . . . . . . 7 (∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
240237, 239sylibr 234 . . . . . 6 (𝜑 → ∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏)
241111sseq1d 4026 . . . . . . . . . 10 (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ 𝑏))
242241rexbidv 3176 . . . . . . . . 9 (𝑝 = 𝐴 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
243242ralbidv 3175 . . . . . . . 8 (𝑝 = 𝐴 → (∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
244243ralsng 4679 . . . . . . 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 7671 . . . . . 6 (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
2485, 87, 247sylancr 587 . . . . 5 (𝜑 → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞𝑌𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
249246, 248mpbird 257 . . . 4 (𝜑 → ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏)
250 ralunb 4206 . . . 4 (∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ↔ (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏 ∧ ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏))
251208, 249, 250sylanbrc 583 . . 3 (𝜑 → ∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎𝑏)
25230, 64, 168, 251cofon2 8709 . 2 (𝜑 {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤} = {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
2534, 252eqtrd 2774 1 (𝜑 → (𝐴 +no 𝐵) = {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847   = wceq 1536  wcel 2105  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cun 3960  wss 3962  𝒫 cpw 4604  {csn 4630   cint 4950   × cxp 5686  ran crn 5689  cima 5691  Oncon0 6385  Fun wfun 6556   Fn wfn 6557  wf 6558  (class class class)co 7430   +no cnadd 8701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-frecs 8304  df-nadd 8702
This theorem is referenced by:  naddasslem1  8730  naddasslem2  8731
  Copyright terms: Public domain W3C validator