MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  naddunif Structured version   Visualization version   GIF version
Theorem naddunif 8687
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 8674 . . 3 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 +no 𝐡) = ∩ {𝑀 ∈ On ∣ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) βŠ† 𝑀})
41, 2, 3syl2anc 583 . 2 (πœ‘ β†’ (𝐴 +no 𝐡) = ∩ {𝑀 ∈ On ∣ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) βŠ† 𝑀})
5 naddfn 8669 . . . . . . 7 +no Fn (On Γ— On)
6 fnfun 6639 . . . . . . 7 ( +no Fn (On Γ— On) β†’ Fun +no )
75, 6ax-mp 5 . . . . . 6 Fun +no
8 snex 5421 . . . . . . 7 {𝐴} ∈ V
9 xpexg 7730 . . . . . . 7 (({𝐴} ∈ V ∧ 𝐡 ∈ On) β†’ ({𝐴} Γ— 𝐡) ∈ V)
108, 2, 9sylancr 586 . . . . . 6 (πœ‘ β†’ ({𝐴} Γ— 𝐡) ∈ V)
11 funimaexg 6624 . . . . . 6 ((Fun +no ∧ ({𝐴} Γ— 𝐡) ∈ V) β†’ ( +no β€œ ({𝐴} Γ— 𝐡)) ∈ V)
127, 10, 11sylancr 586 . . . . 5 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— 𝐡)) ∈ V)
13 imassrn 6060 . . . . . . 7 ( +no β€œ ({𝐴} Γ— 𝐡)) βŠ† ran +no
14 naddf 8675 . . . . . . . 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 3983 . . . . . 6 ( +no β€œ ({𝐴} Γ— 𝐡)) βŠ† On
1817a1i 11 . . . . 5 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— 𝐡)) βŠ† On)
1912, 18elpwd 4600 . . . 4 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— 𝐡)) ∈ 𝒫 On)
20 snex 5421 . . . . . . 7 {𝐡} ∈ V
21 xpexg 7730 . . . . . . 7 ((𝐴 ∈ On ∧ {𝐡} ∈ V) β†’ (𝐴 Γ— {𝐡}) ∈ V)
221, 20, 21sylancl 585 . . . . . 6 (πœ‘ β†’ (𝐴 Γ— {𝐡}) ∈ V)
23 funimaexg 6624 . . . . . 6 ((Fun +no ∧ (𝐴 Γ— {𝐡}) ∈ V) β†’ ( +no β€œ (𝐴 Γ— {𝐡})) ∈ V)
247, 22, 23sylancr 586 . . . . 5 (πœ‘ β†’ ( +no β€œ (𝐴 Γ— {𝐡})) ∈ V)
25 imassrn 6060 . . . . . . 7 ( +no β€œ (𝐴 Γ— {𝐡})) βŠ† ran +no
2625, 16sstri 3983 . . . . . 6 ( +no β€œ (𝐴 Γ— {𝐡})) βŠ† On
2726a1i 11 . . . . 5 (πœ‘ β†’ ( +no β€œ (𝐴 Γ— {𝐡})) βŠ† On)
2824, 27elpwd 4600 . . . 4 (πœ‘ β†’ ( +no β€œ (𝐴 Γ— {𝐡})) ∈ 𝒫 On)
29 pwuncl 7750 . . . 4 ((( +no β€œ ({𝐴} Γ— 𝐡)) ∈ 𝒫 On ∧ ( +no β€œ (𝐴 Γ— {𝐡})) ∈ 𝒫 On) β†’ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) ∈ 𝒫 On)
3019, 28, 29syl2anc 583 . . 3 (πœ‘ β†’ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) ∈ 𝒫 On)
31 naddunif.3 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 = ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯})
3231, 1eqeltrrd 2826 . . . . . . . . 9 (πœ‘ β†’ ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯} ∈ On)
33 onintrab2 7778 . . . . . . . . 9 (βˆƒπ‘₯ ∈ On 𝑋 βŠ† π‘₯ ↔ ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯} ∈ On)
3432, 33sylibr 233 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘₯ ∈ On 𝑋 βŠ† π‘₯)
35 vex 3470 . . . . . . . . . 10 π‘₯ ∈ V
3635ssex 5311 . . . . . . . . 9 (𝑋 βŠ† π‘₯ β†’ 𝑋 ∈ V)
3736rexlimivw 3143 . . . . . . . 8 (βˆƒπ‘₯ ∈ On 𝑋 βŠ† π‘₯ β†’ 𝑋 ∈ V)
3834, 37syl 17 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ V)
39 xpexg 7730 . . . . . . 7 ((𝑋 ∈ V ∧ {𝐡} ∈ V) β†’ (𝑋 Γ— {𝐡}) ∈ V)
4038, 20, 39sylancl 585 . . . . . 6 (πœ‘ β†’ (𝑋 Γ— {𝐡}) ∈ V)
41 funimaexg 6624 . . . . . 6 ((Fun +no ∧ (𝑋 Γ— {𝐡}) ∈ V) β†’ ( +no β€œ (𝑋 Γ— {𝐡})) ∈ V)
427, 40, 41sylancr 586 . . . . 5 (πœ‘ β†’ ( +no β€œ (𝑋 Γ— {𝐡})) ∈ V)
43 imassrn 6060 . . . . . . 7 ( +no β€œ (𝑋 Γ— {𝐡})) βŠ† ran +no
4443, 16sstri 3983 . . . . . 6 ( +no β€œ (𝑋 Γ— {𝐡})) βŠ† On
4544a1i 11 . . . . 5 (πœ‘ β†’ ( +no β€œ (𝑋 Γ— {𝐡})) βŠ† On)
4642, 45elpwd 4600 . . . 4 (πœ‘ β†’ ( +no β€œ (𝑋 Γ— {𝐡})) ∈ 𝒫 On)
47 naddunif.4 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 = ∩ {𝑦 ∈ On ∣ π‘Œ βŠ† 𝑦})
4847, 2eqeltrrd 2826 . . . . . . . . 9 (πœ‘ β†’ ∩ {𝑦 ∈ On ∣ π‘Œ βŠ† 𝑦} ∈ On)
49 onintrab2 7778 . . . . . . . . 9 (βˆƒπ‘¦ ∈ On π‘Œ βŠ† 𝑦 ↔ ∩ {𝑦 ∈ On ∣ π‘Œ βŠ† 𝑦} ∈ On)
5048, 49sylibr 233 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘¦ ∈ On π‘Œ βŠ† 𝑦)
51 vex 3470 . . . . . . . . . 10 𝑦 ∈ V
5251ssex 5311 . . . . . . . . 9 (π‘Œ βŠ† 𝑦 β†’ π‘Œ ∈ V)
5352rexlimivw 3143 . . . . . . . 8 (βˆƒπ‘¦ ∈ On π‘Œ βŠ† 𝑦 β†’ π‘Œ ∈ V)
5450, 53syl 17 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ V)
55 xpexg 7730 . . . . . . 7 (({𝐴} ∈ V ∧ π‘Œ ∈ V) β†’ ({𝐴} Γ— π‘Œ) ∈ V)
568, 54, 55sylancr 586 . . . . . 6 (πœ‘ β†’ ({𝐴} Γ— π‘Œ) ∈ V)
57 funimaexg 6624 . . . . . 6 ((Fun +no ∧ ({𝐴} Γ— π‘Œ) ∈ V) β†’ ( +no β€œ ({𝐴} Γ— π‘Œ)) ∈ V)
587, 56, 57sylancr 586 . . . . 5 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— π‘Œ)) ∈ V)
59 imassrn 6060 . . . . . . 7 ( +no β€œ ({𝐴} Γ— π‘Œ)) βŠ† ran +no
6059, 16sstri 3983 . . . . . 6 ( +no β€œ ({𝐴} Γ— π‘Œ)) βŠ† On
6160a1i 11 . . . . 5 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— π‘Œ)) βŠ† On)
6258, 61elpwd 4600 . . . 4 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— π‘Œ)) ∈ 𝒫 On)
63 pwuncl 7750 . . . 4 ((( +no β€œ (𝑋 Γ— {𝐡})) ∈ 𝒫 On ∧ ( +no β€œ ({𝐴} Γ— π‘Œ)) ∈ 𝒫 On) β†’ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ))) ∈ 𝒫 On)
6446, 62, 63syl2anc 583 . . 3 (πœ‘ β†’ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ))) ∈ 𝒫 On)
652, 47cofonr 8668 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ π‘ž βŠ† 𝑠)
66 onss 7765 . . . . . . . . . . . . . . 15 (𝐡 ∈ On β†’ 𝐡 βŠ† On)
672, 66syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐡 βŠ† On)
6867sselda 3974 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐡) β†’ π‘ž ∈ On)
6968adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐡) ∧ 𝑠 ∈ π‘Œ) β†’ π‘ž ∈ On)
70 onss 7765 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ On β†’ 𝑦 βŠ† On)
7170adantl 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ On) β†’ 𝑦 βŠ† On)
72 sstr 3982 . . . . . . . . . . . . . . . . . 18 ((π‘Œ βŠ† 𝑦 ∧ 𝑦 βŠ† On) β†’ π‘Œ βŠ† On)
7372expcom 413 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ (π‘Œ βŠ† 𝑦 β†’ π‘Œ βŠ† On))
7471, 73syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ On) β†’ (π‘Œ βŠ† 𝑦 β†’ π‘Œ βŠ† On))
7574rexlimdva 3147 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆƒπ‘¦ ∈ On π‘Œ βŠ† 𝑦 β†’ π‘Œ βŠ† On))
7650, 75mpd 15 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ βŠ† On)
7776adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐡) β†’ π‘Œ βŠ† On)
7877sselda 3974 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐡) ∧ 𝑠 ∈ π‘Œ) β†’ 𝑠 ∈ On)
791ad2antrr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐡) ∧ 𝑠 ∈ π‘Œ) β†’ 𝐴 ∈ On)
80 naddss2 8684 . . . . . . . . . . . 12 ((π‘ž ∈ On ∧ 𝑠 ∈ On ∧ 𝐴 ∈ On) β†’ (π‘ž βŠ† 𝑠 ↔ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
8169, 78, 79, 80syl3anc 1368 . . . . . . . . . . 11 (((πœ‘ ∧ π‘ž ∈ 𝐡) ∧ 𝑠 ∈ π‘Œ) β†’ (π‘ž βŠ† 𝑠 ↔ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
8281rexbidva 3168 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ 𝐡) β†’ (βˆƒπ‘  ∈ π‘Œ π‘ž βŠ† 𝑠 ↔ βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
8382ralbidva 3167 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ π‘ž βŠ† 𝑠 ↔ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
8465, 83mpbid 231 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠))
851snssd 4804 . . . . . . . . . . . 12 (πœ‘ β†’ {𝐴} βŠ† On)
86 xpss12 5681 . . . . . . . . . . . 12 (({𝐴} βŠ† On ∧ π‘Œ βŠ† On) β†’ ({𝐴} Γ— π‘Œ) βŠ† (On Γ— On))
8785, 76, 86syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ ({𝐴} Γ— π‘Œ) βŠ† (On Γ— On))
88 sseq2 4000 . . . . . . . . . . . 12 (𝑑 = (π‘Ÿ +no 𝑠) β†’ ((𝐴 +no π‘ž) βŠ† 𝑑 ↔ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
8988imaeqexov 7638 . . . . . . . . . . 11 (( +no Fn (On Γ— On) ∧ ({𝐴} Γ— π‘Œ) βŠ† (On Γ— On)) β†’ (βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
905, 87, 89sylancr 586 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
91 oveq1 7408 . . . . . . . . . . . . . 14 (π‘Ÿ = 𝐴 β†’ (π‘Ÿ +no 𝑠) = (𝐴 +no 𝑠))
9291sseq2d 4006 . . . . . . . . . . . . 13 (π‘Ÿ = 𝐴 β†’ ((𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
9392rexbidv 3170 . . . . . . . . . . . 12 (π‘Ÿ = 𝐴 β†’ (βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
9493rexsng 4670 . . . . . . . . . . 11 (𝐴 ∈ On β†’ (βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
951, 94syl 17 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
9690, 95bitrd 279 . . . . . . . . 9 (πœ‘ β†’ (βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
9796ralbidv 3169 . . . . . . . 8 (πœ‘ β†’ (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
9884, 97mpbird 257 . . . . . . 7 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑)
99 olc 865 . . . . . . . 8 (βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
10099ralimi 3075 . . . . . . 7 (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 β†’ βˆ€π‘ž ∈ 𝐡 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
10198, 100syl 17 . . . . . 6 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
102 rexun 4182 . . . . . . 7 (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
103102ralbii 3085 . . . . . 6 (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ βˆ€π‘ž ∈ 𝐡 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
104101, 103sylibr 233 . . . . 5 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑)
105 xpss12 5681 . . . . . . . 8 (({𝐴} βŠ† On ∧ 𝐡 βŠ† On) β†’ ({𝐴} Γ— 𝐡) βŠ† (On Γ— On))
10685, 67, 105syl2anc 583 . . . . . . 7 (πœ‘ β†’ ({𝐴} Γ— 𝐡) βŠ† (On Γ— On))
107 sseq1 3999 . . . . . . . . 9 (𝑐 = (𝑝 +no π‘ž) β†’ (𝑐 βŠ† 𝑑 ↔ (𝑝 +no π‘ž) βŠ† 𝑑))
108107rexbidv 3170 . . . . . . . 8 (𝑐 = (𝑝 +no π‘ž) β†’ (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ↔ βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑))
109108imaeqalov 7639 . . . . . . 7 (( +no Fn (On Γ— On) ∧ ({𝐴} Γ— 𝐡) βŠ† (On Γ— On)) β†’ (βˆ€π‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ↔ βˆ€π‘ ∈ {𝐴}βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑))
1105, 106, 109sylancr 586 . . . . . 6 (πœ‘ β†’ (βˆ€π‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ↔ βˆ€π‘ ∈ {𝐴}βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑))
111 oveq1 7408 . . . . . . . . . . 11 (𝑝 = 𝐴 β†’ (𝑝 +no π‘ž) = (𝐴 +no π‘ž))
112111sseq1d 4005 . . . . . . . . . 10 (𝑝 = 𝐴 β†’ ((𝑝 +no π‘ž) βŠ† 𝑑 ↔ (𝐴 +no π‘ž) βŠ† 𝑑))
113112rexbidv 3170 . . . . . . . . 9 (𝑝 = 𝐴 β†’ (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑))
114113ralbidv 3169 . . . . . . . 8 (𝑝 = 𝐴 β†’ (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑))
115114ralsng 4669 . . . . . . 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 8668 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 𝑝 βŠ† π‘Ÿ)
120 onss 7765 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On β†’ 𝐴 βŠ† On)
1211, 120syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 βŠ† On)
122121sselda 3974 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ 𝑝 ∈ On)
123122adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝐴) ∧ π‘Ÿ ∈ 𝑋) β†’ 𝑝 ∈ On)
124 ssintub 4960 . . . . . . . . . . . . . . . 16 𝑋 βŠ† ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯}
12531, 121eqsstrrd 4013 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯} βŠ† On)
126124, 125sstrid 3985 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 βŠ† On)
127126adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ 𝑋 βŠ† On)
128127sselda 3974 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝐴) ∧ π‘Ÿ ∈ 𝑋) β†’ π‘Ÿ ∈ On)
1292ad2antrr 723 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝐴) ∧ π‘Ÿ ∈ 𝑋) β†’ 𝐡 ∈ On)
130 naddss1 8683 . . . . . . . . . . . . 13 ((𝑝 ∈ On ∧ π‘Ÿ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑝 βŠ† π‘Ÿ ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
131123, 128, 129, 130syl3anc 1368 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝐴) ∧ π‘Ÿ ∈ 𝑋) β†’ (𝑝 βŠ† π‘Ÿ ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
132131rexbidva 3168 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ (βˆƒπ‘Ÿ ∈ 𝑋 𝑝 βŠ† π‘Ÿ ↔ βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
133132ralbidva 3167 . . . . . . . . . 10 (πœ‘ β†’ (βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 𝑝 βŠ† π‘Ÿ ↔ βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
134119, 133mpbid 231 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡))
1352snssd 4804 . . . . . . . . . . . . 13 (πœ‘ β†’ {𝐡} βŠ† On)
136 xpss12 5681 . . . . . . . . . . . . 13 ((𝑋 βŠ† On ∧ {𝐡} βŠ† On) β†’ (𝑋 Γ— {𝐡}) βŠ† (On Γ— On))
137126, 135, 136syl2anc 583 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑋 Γ— {𝐡}) βŠ† (On Γ— On))
138 sseq2 4000 . . . . . . . . . . . . 13 (𝑑 = (π‘Ÿ +no 𝑠) β†’ ((𝑝 +no 𝐡) βŠ† 𝑑 ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
139138imaeqexov 7638 . . . . . . . . . . . 12 (( +no Fn (On Γ— On) ∧ (𝑋 Γ— {𝐡}) βŠ† (On Γ— On)) β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ 𝑋 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
1405, 137, 139sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ 𝑋 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
141 oveq2 7409 . . . . . . . . . . . . . . 15 (𝑠 = 𝐡 β†’ (π‘Ÿ +no 𝑠) = (π‘Ÿ +no 𝐡))
142141sseq2d 4006 . . . . . . . . . . . . . 14 (𝑠 = 𝐡 β†’ ((𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠) ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
143142rexsng 4670 . . . . . . . . . . . . 13 (𝐡 ∈ On β†’ (βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠) ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
1442, 143syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠) ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
145144rexbidv 3170 . . . . . . . . . . 11 (πœ‘ β†’ (βˆƒπ‘Ÿ ∈ 𝑋 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
146140, 145bitrd 279 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
147146ralbidv 3169 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
148134, 147mpbird 257 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑)
149 orc 864 . . . . . . . . 9 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
150149ralimi 3075 . . . . . . . 8 (βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 β†’ βˆ€π‘ ∈ 𝐴 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
151148, 150syl 17 . . . . . . 7 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
152 rexun 4182 . . . . . . . 8 (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
153152ralbii 3085 . . . . . . 7 (βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ βˆ€π‘ ∈ 𝐴 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
154151, 153sylibr 233 . . . . . 6 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑)
155 oveq2 7409 . . . . . . . . . . 11 (π‘ž = 𝐡 β†’ (𝑝 +no π‘ž) = (𝑝 +no 𝐡))
156155sseq1d 4005 . . . . . . . . . 10 (π‘ž = 𝐡 β†’ ((𝑝 +no π‘ž) βŠ† 𝑑 ↔ (𝑝 +no 𝐡) βŠ† 𝑑))
157156rexbidv 3170 . . . . . . . . 9 (π‘ž = 𝐡 β†’ (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑))
158157ralsng 4669 . . . . . . . 8 (𝐡 ∈ On β†’ (βˆ€π‘ž ∈ {𝐡}βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑))
1592, 158syl 17 . . . . . . 7 (πœ‘ β†’ (βˆ€π‘ž ∈ {𝐡}βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑))
160159ralbidv 3169 . . . . . 6 (πœ‘ β†’ (βˆ€π‘ ∈ 𝐴 βˆ€π‘ž ∈ {𝐡}βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑))
161154, 160mpbird 257 . . . . 5 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 βˆ€π‘ž ∈ {𝐡}βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑)
162 xpss12 5681 . . . . . . 7 ((𝐴 βŠ† On ∧ {𝐡} βŠ† On) β†’ (𝐴 Γ— {𝐡}) βŠ† (On Γ— On))
163121, 135, 162syl2anc 583 . . . . . 6 (πœ‘ β†’ (𝐴 Γ— {𝐡}) βŠ† (On Γ— On))
164108imaeqalov 7639 . . . . . 6 (( +no Fn (On Γ— On) ∧ (𝐴 Γ— {𝐡}) βŠ† (On Γ— On)) β†’ (βˆ€π‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ↔ βˆ€π‘ ∈ 𝐴 βˆ€π‘ž ∈ {𝐡}βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑))
1655, 163, 164sylancr 586 . . . . 5 (πœ‘ β†’ (βˆ€π‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ↔ βˆ€π‘ ∈ 𝐴 βˆ€π‘ž ∈ {𝐡}βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑))
166161, 165mpbird 257 . . . 4 (πœ‘ β†’ βˆ€π‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑)
167 ralunb 4183 . . . 4 (βˆ€π‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ↔ (βˆ€π‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ∧ βˆ€π‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑))
168118, 166, 167sylanbrc 582 . . 3 (πœ‘ β†’ βˆ€π‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑)
169124, 31sseqtrrid 4027 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 βŠ† 𝐴)
170169sselda 3974 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ 𝑝 ∈ 𝐴)
171 ssid 3996 . . . . . . . . . . 11 𝑝 βŠ† 𝑝
172 sseq2 4000 . . . . . . . . . . . 12 (π‘Ÿ = 𝑝 β†’ (𝑝 βŠ† π‘Ÿ ↔ 𝑝 βŠ† 𝑝))
173172rspcev 3604 . . . . . . . . . . 11 ((𝑝 ∈ 𝐴 ∧ 𝑝 βŠ† 𝑝) β†’ βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ)
174170, 171, 173sylancl 585 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ)
175174ralrimiva 3138 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ)
176126sselda 3974 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ 𝑝 ∈ On)
177176adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑋) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑝 ∈ On)
178121adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ 𝐴 βŠ† On)
179178sselda 3974 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑋) ∧ π‘Ÿ ∈ 𝐴) β†’ π‘Ÿ ∈ On)
1802ad2antrr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑋) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝐡 ∈ On)
181177, 179, 180, 130syl3anc 1368 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ 𝑋) ∧ π‘Ÿ ∈ 𝐴) β†’ (𝑝 βŠ† π‘Ÿ ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
182181rexbidva 3168 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ (βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ ↔ βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
183182ralbidva 3167 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ ↔ βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
184175, 183mpbid 231 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡))
185 sseq2 4000 . . . . . . . . . . . 12 (𝑏 = (π‘Ÿ +no 𝑠) β†’ ((𝑝 +no 𝐡) βŠ† 𝑏 ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
186185imaeqexov 7638 . . . . . . . . . . 11 (( +no Fn (On Γ— On) ∧ (𝐴 Γ— {𝐡}) βŠ† (On Γ— On)) β†’ (βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 ↔ βˆƒπ‘Ÿ ∈ 𝐴 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
1875, 163, 186sylancr 586 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 ↔ βˆƒπ‘Ÿ ∈ 𝐴 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
188144rexbidv 3170 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘Ÿ ∈ 𝐴 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
189187, 188bitrd 279 . . . . . . . . 9 (πœ‘ β†’ (βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 ↔ βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
190189ralbidv 3169 . . . . . . . 8 (πœ‘ β†’ (βˆ€π‘ ∈ 𝑋 βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 ↔ βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
191184, 190mpbird 257 . . . . . . 7 (πœ‘ β†’ βˆ€π‘ ∈ 𝑋 βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏)
192 olc 865 . . . . . . . 8 (βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 β†’ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏))
193192ralimi 3075 . . . . . . 7 (βˆ€π‘ ∈ 𝑋 βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 β†’ βˆ€π‘ ∈ 𝑋 (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏))
194191, 193syl 17 . . . . . 6 (πœ‘ β†’ βˆ€π‘ ∈ 𝑋 (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏))
195155sseq1d 4005 . . . . . . . . . . . 12 (π‘ž = 𝐡 β†’ ((𝑝 +no π‘ž) βŠ† 𝑏 ↔ (𝑝 +no 𝐡) βŠ† 𝑏))
196195rexbidv 3170 . . . . . . . . . . 11 (π‘ž = 𝐡 β†’ (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏 ↔ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no 𝐡) βŠ† 𝑏))
197196ralsng 4669 . . . . . . . . . 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 4182 . . . . . . . 8 (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no 𝐡) βŠ† 𝑏 ↔ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏))
201199, 200bitrdi 287 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ (βˆ€π‘ž ∈ {𝐡}βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏 ↔ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏)))
202201ralbidva 3167 . . . . . 6 (πœ‘ β†’ (βˆ€π‘ ∈ 𝑋 βˆ€π‘ž ∈ {𝐡}βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏 ↔ βˆ€π‘ ∈ 𝑋 (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏)))
203194, 202mpbird 257 . . . . 5 (πœ‘ β†’ βˆ€π‘ ∈ 𝑋 βˆ€π‘ž ∈ {𝐡}βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏)
204 sseq1 3999 . . . . . . . 8 (π‘Ž = (𝑝 +no π‘ž) β†’ (π‘Ž βŠ† 𝑏 ↔ (𝑝 +no π‘ž) βŠ† 𝑏))
205204rexbidv 3170 . . . . . . 7 (π‘Ž = (𝑝 +no π‘ž) β†’ (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ↔ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏))
206205imaeqalov 7639 . . . . . 6 (( +no Fn (On Γ— On) ∧ (𝑋 Γ— {𝐡}) βŠ† (On Γ— On)) β†’ (βˆ€π‘Ž ∈ ( +no β€œ (𝑋 Γ— {𝐡}))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ↔ βˆ€π‘ ∈ 𝑋 βˆ€π‘ž ∈ {𝐡}βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏))
2075, 137, 206sylancr 586 . . . . 5 (πœ‘ β†’ (βˆ€π‘Ž ∈ ( +no β€œ (𝑋 Γ— {𝐡}))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ↔ βˆ€π‘ ∈ 𝑋 βˆ€π‘ž ∈ {𝐡}βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏))
208203, 207mpbird 257 . . . 4 (πœ‘ β†’ βˆ€π‘Ž ∈ ( +no β€œ (𝑋 Γ— {𝐡}))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏)
209 ssintub 4960 . . . . . . . . . . . . 13 π‘Œ βŠ† ∩ {𝑦 ∈ On ∣ π‘Œ βŠ† 𝑦}
210209, 47sseqtrrid 4027 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ βŠ† 𝐡)
211210sselda 3974 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ π‘ž ∈ 𝐡)
212 ssid 3996 . . . . . . . . . . 11 π‘ž βŠ† π‘ž
213 sseq2 4000 . . . . . . . . . . . 12 (𝑠 = π‘ž β†’ (π‘ž βŠ† 𝑠 ↔ π‘ž βŠ† π‘ž))
214213rspcev 3604 . . . . . . . . . . 11 ((π‘ž ∈ 𝐡 ∧ π‘ž βŠ† π‘ž) β†’ βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠)
215211, 212, 214sylancl 585 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠)
216215ralrimiva 3138 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘ž ∈ π‘Œ βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠)
21792rexbidv 3170 . . . . . . . . . . . . . 14 (π‘Ÿ = 𝐴 β†’ (βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
218217rexsng 4670 . . . . . . . . . . . . 13 (𝐴 ∈ On β†’ (βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
2191, 218syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
220219adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ (βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
221 sseq2 4000 . . . . . . . . . . . . . 14 (𝑏 = (π‘Ÿ +no 𝑠) β†’ ((𝐴 +no π‘ž) βŠ† 𝑏 ↔ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
222221imaeqexov 7638 . . . . . . . . . . . . 13 (( +no Fn (On Γ— On) ∧ ({𝐴} Γ— 𝐡) βŠ† (On Γ— On)) β†’ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
2235, 106, 222sylancr 586 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
224223adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
22576sselda 3974 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ π‘ž ∈ On)
226225adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘ž ∈ π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ π‘ž ∈ On)
22767adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ 𝐡 βŠ† On)
228227sselda 3974 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘ž ∈ π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 ∈ On)
2291ad2antrr 723 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘ž ∈ π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ 𝐴 ∈ On)
230226, 228, 229, 80syl3anc 1368 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ (π‘ž βŠ† 𝑠 ↔ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
231230rexbidva 3168 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ (βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠 ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
232220, 224, 2313bitr4d 311 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠))
233232ralbidva 3167 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ βˆ€π‘ž ∈ π‘Œ βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠))
234216, 233mpbird 257 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏)
235 orc 864 . . . . . . . . 9 (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 β†’ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
236235ralimi 3075 . . . . . . . 8 (βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 β†’ βˆ€π‘ž ∈ π‘Œ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
237234, 236syl 17 . . . . . . 7 (πœ‘ β†’ βˆ€π‘ž ∈ π‘Œ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
238 rexun 4182 . . . . . . . 8 (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
239238ralbii 3085 . . . . . . 7 (βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ βˆ€π‘ž ∈ π‘Œ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
240237, 239sylibr 233 . . . . . 6 (πœ‘ β†’ βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏)
241111sseq1d 4005 . . . . . . . . . 10 (𝑝 = 𝐴 β†’ ((𝑝 +no π‘ž) βŠ† 𝑏 ↔ (𝐴 +no π‘ž) βŠ† 𝑏))
242241rexbidv 3170 . . . . . . . . 9 (𝑝 = 𝐴 β†’ (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏 ↔ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏))
243242ralbidv 3169 . . . . . . . 8 (𝑝 = 𝐴 β†’ (βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏 ↔ βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏))
244243ralsng 4669 . . . . . . 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 7639 . . . . . 6 (( +no Fn (On Γ— On) ∧ ({𝐴} Γ— π‘Œ) βŠ† (On Γ— On)) β†’ (βˆ€π‘Ž ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ↔ βˆ€π‘ ∈ {𝐴}βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏))
2485, 87, 247sylancr 586 . . . . 5 (πœ‘ β†’ (βˆ€π‘Ž ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ↔ βˆ€π‘ ∈ {𝐴}βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏))
249246, 248mpbird 257 . . . 4 (πœ‘ β†’ βˆ€π‘Ž ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏)
250 ralunb 4183 . . . 4 (βˆ€π‘Ž ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ↔ (βˆ€π‘Ž ∈ ( +no β€œ (𝑋 Γ— {𝐡}))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ∧ βˆ€π‘Ž ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏))
251208, 249, 250sylanbrc 582 . . 3 (πœ‘ β†’ βˆ€π‘Ž ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏)
25230, 64, 168, 251cofon2 8667 . 2 (πœ‘ β†’ ∩ {𝑀 ∈ On ∣ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) βŠ† 𝑀} = ∩ {𝑧 ∈ On ∣ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ))) βŠ† 𝑧})
2534, 252eqtrd 2764 1 (πœ‘ β†’ (𝐴 +no 𝐡) = ∩ {𝑧 ∈ On ∣ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ))) βŠ† 𝑧})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1533   ∈ wcel 2098  βˆ€wral 3053  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βˆͺ cun 3938   βŠ† wss 3940  π’« cpw 4594  {csn 4620  βˆ© cint 4940   Γ— cxp 5664  ran crn 5667   β€œ cima 5669  Oncon0 6354  Fun wfun 6527   Fn wfn 6528  βŸΆwf 6529  (class class class)co 7401   +no cnadd 8659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-nadd 8660
This theorem is referenced by:  naddasslem1  8688  naddasslem2  8689
  Copyright terms: Public domain W3C validator