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

Theorem naddunif 8638
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 8627 . . 3 ((𝐴 ∈ On ∧ 𝐡 ∈ On) β†’ (𝐴 +no 𝐡) = ∩ {𝑀 ∈ On ∣ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) βŠ† 𝑀})
41, 2, 3syl2anc 585 . 2 (πœ‘ β†’ (𝐴 +no 𝐡) = ∩ {𝑀 ∈ On ∣ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) βŠ† 𝑀})
5 naddfn 8622 . . . . . . 7 +no Fn (On Γ— On)
6 fnfun 6603 . . . . . . 7 ( +no Fn (On Γ— On) β†’ Fun +no )
75, 6ax-mp 5 . . . . . 6 Fun +no
8 snex 5389 . . . . . . 7 {𝐴} ∈ V
9 xpexg 7685 . . . . . . 7 (({𝐴} ∈ V ∧ 𝐡 ∈ On) β†’ ({𝐴} Γ— 𝐡) ∈ V)
108, 2, 9sylancr 588 . . . . . 6 (πœ‘ β†’ ({𝐴} Γ— 𝐡) ∈ V)
11 funimaexg 6588 . . . . . 6 ((Fun +no ∧ ({𝐴} Γ— 𝐡) ∈ V) β†’ ( +no β€œ ({𝐴} Γ— 𝐡)) ∈ V)
127, 10, 11sylancr 588 . . . . 5 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— 𝐡)) ∈ V)
13 imassrn 6025 . . . . . . 7 ( +no β€œ ({𝐴} Γ— 𝐡)) βŠ† ran +no
14 naddf 8628 . . . . . . . 8 +no :(On Γ— On)⟢On
15 frn 6676 . . . . . . . 8 ( +no :(On Γ— On)⟢On β†’ ran +no βŠ† On)
1614, 15ax-mp 5 . . . . . . 7 ran +no βŠ† On
1713, 16sstri 3954 . . . . . 6 ( +no β€œ ({𝐴} Γ— 𝐡)) βŠ† On
1817a1i 11 . . . . 5 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— 𝐡)) βŠ† On)
1912, 18elpwd 4567 . . . 4 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— 𝐡)) ∈ 𝒫 On)
20 snex 5389 . . . . . . 7 {𝐡} ∈ V
21 xpexg 7685 . . . . . . 7 ((𝐴 ∈ On ∧ {𝐡} ∈ V) β†’ (𝐴 Γ— {𝐡}) ∈ V)
221, 20, 21sylancl 587 . . . . . 6 (πœ‘ β†’ (𝐴 Γ— {𝐡}) ∈ V)
23 funimaexg 6588 . . . . . 6 ((Fun +no ∧ (𝐴 Γ— {𝐡}) ∈ V) β†’ ( +no β€œ (𝐴 Γ— {𝐡})) ∈ V)
247, 22, 23sylancr 588 . . . . 5 (πœ‘ β†’ ( +no β€œ (𝐴 Γ— {𝐡})) ∈ V)
25 imassrn 6025 . . . . . . 7 ( +no β€œ (𝐴 Γ— {𝐡})) βŠ† ran +no
2625, 16sstri 3954 . . . . . 6 ( +no β€œ (𝐴 Γ— {𝐡})) βŠ† On
2726a1i 11 . . . . 5 (πœ‘ β†’ ( +no β€œ (𝐴 Γ— {𝐡})) βŠ† On)
2824, 27elpwd 4567 . . . 4 (πœ‘ β†’ ( +no β€œ (𝐴 Γ— {𝐡})) ∈ 𝒫 On)
29 pwuncl 7705 . . . 4 ((( +no β€œ ({𝐴} Γ— 𝐡)) ∈ 𝒫 On ∧ ( +no β€œ (𝐴 Γ— {𝐡})) ∈ 𝒫 On) β†’ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) ∈ 𝒫 On)
3019, 28, 29syl2anc 585 . . 3 (πœ‘ β†’ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) ∈ 𝒫 On)
31 naddunif.3 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 = ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯})
3231, 1eqeltrrd 2839 . . . . . . . . 9 (πœ‘ β†’ ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯} ∈ On)
33 onintrab2 7733 . . . . . . . . 9 (βˆƒπ‘₯ ∈ On 𝑋 βŠ† π‘₯ ↔ ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯} ∈ On)
3432, 33sylibr 233 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘₯ ∈ On 𝑋 βŠ† π‘₯)
35 vex 3450 . . . . . . . . . 10 π‘₯ ∈ V
3635ssex 5279 . . . . . . . . 9 (𝑋 βŠ† π‘₯ β†’ 𝑋 ∈ V)
3736rexlimivw 3149 . . . . . . . 8 (βˆƒπ‘₯ ∈ On 𝑋 βŠ† π‘₯ β†’ 𝑋 ∈ V)
3834, 37syl 17 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ V)
39 xpexg 7685 . . . . . . 7 ((𝑋 ∈ V ∧ {𝐡} ∈ V) β†’ (𝑋 Γ— {𝐡}) ∈ V)
4038, 20, 39sylancl 587 . . . . . 6 (πœ‘ β†’ (𝑋 Γ— {𝐡}) ∈ V)
41 funimaexg 6588 . . . . . 6 ((Fun +no ∧ (𝑋 Γ— {𝐡}) ∈ V) β†’ ( +no β€œ (𝑋 Γ— {𝐡})) ∈ V)
427, 40, 41sylancr 588 . . . . 5 (πœ‘ β†’ ( +no β€œ (𝑋 Γ— {𝐡})) ∈ V)
43 imassrn 6025 . . . . . . 7 ( +no β€œ (𝑋 Γ— {𝐡})) βŠ† ran +no
4443, 16sstri 3954 . . . . . 6 ( +no β€œ (𝑋 Γ— {𝐡})) βŠ† On
4544a1i 11 . . . . 5 (πœ‘ β†’ ( +no β€œ (𝑋 Γ— {𝐡})) βŠ† On)
4642, 45elpwd 4567 . . . 4 (πœ‘ β†’ ( +no β€œ (𝑋 Γ— {𝐡})) ∈ 𝒫 On)
47 naddunif.4 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 = ∩ {𝑦 ∈ On ∣ π‘Œ βŠ† 𝑦})
4847, 2eqeltrrd 2839 . . . . . . . . 9 (πœ‘ β†’ ∩ {𝑦 ∈ On ∣ π‘Œ βŠ† 𝑦} ∈ On)
49 onintrab2 7733 . . . . . . . . 9 (βˆƒπ‘¦ ∈ On π‘Œ βŠ† 𝑦 ↔ ∩ {𝑦 ∈ On ∣ π‘Œ βŠ† 𝑦} ∈ On)
5048, 49sylibr 233 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘¦ ∈ On π‘Œ βŠ† 𝑦)
51 vex 3450 . . . . . . . . . 10 𝑦 ∈ V
5251ssex 5279 . . . . . . . . 9 (π‘Œ βŠ† 𝑦 β†’ π‘Œ ∈ V)
5352rexlimivw 3149 . . . . . . . 8 (βˆƒπ‘¦ ∈ On π‘Œ βŠ† 𝑦 β†’ π‘Œ ∈ V)
5450, 53syl 17 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ V)
55 xpexg 7685 . . . . . . 7 (({𝐴} ∈ V ∧ π‘Œ ∈ V) β†’ ({𝐴} Γ— π‘Œ) ∈ V)
568, 54, 55sylancr 588 . . . . . 6 (πœ‘ β†’ ({𝐴} Γ— π‘Œ) ∈ V)
57 funimaexg 6588 . . . . . 6 ((Fun +no ∧ ({𝐴} Γ— π‘Œ) ∈ V) β†’ ( +no β€œ ({𝐴} Γ— π‘Œ)) ∈ V)
587, 56, 57sylancr 588 . . . . 5 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— π‘Œ)) ∈ V)
59 imassrn 6025 . . . . . . 7 ( +no β€œ ({𝐴} Γ— π‘Œ)) βŠ† ran +no
6059, 16sstri 3954 . . . . . 6 ( +no β€œ ({𝐴} Γ— π‘Œ)) βŠ† On
6160a1i 11 . . . . 5 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— π‘Œ)) βŠ† On)
6258, 61elpwd 4567 . . . 4 (πœ‘ β†’ ( +no β€œ ({𝐴} Γ— π‘Œ)) ∈ 𝒫 On)
63 pwuncl 7705 . . . 4 ((( +no β€œ (𝑋 Γ— {𝐡})) ∈ 𝒫 On ∧ ( +no β€œ ({𝐴} Γ— π‘Œ)) ∈ 𝒫 On) β†’ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ))) ∈ 𝒫 On)
6446, 62, 63syl2anc 585 . . 3 (πœ‘ β†’ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ))) ∈ 𝒫 On)
652, 47cofonr 8621 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ π‘ž βŠ† 𝑠)
66 onss 7720 . . . . . . . . . . . . . . 15 (𝐡 ∈ On β†’ 𝐡 βŠ† On)
672, 66syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐡 βŠ† On)
6867sselda 3945 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐡) β†’ π‘ž ∈ On)
6968adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐡) ∧ 𝑠 ∈ π‘Œ) β†’ π‘ž ∈ On)
70 onss 7720 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ On β†’ 𝑦 βŠ† On)
7170adantl 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ On) β†’ 𝑦 βŠ† On)
72 sstr 3953 . . . . . . . . . . . . . . . . . 18 ((π‘Œ βŠ† 𝑦 ∧ 𝑦 βŠ† On) β†’ π‘Œ βŠ† On)
7372expcom 415 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ (π‘Œ βŠ† 𝑦 β†’ π‘Œ βŠ† On))
7471, 73syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ On) β†’ (π‘Œ βŠ† 𝑦 β†’ π‘Œ βŠ† On))
7574rexlimdva 3153 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆƒπ‘¦ ∈ On π‘Œ βŠ† 𝑦 β†’ π‘Œ βŠ† On))
7650, 75mpd 15 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ βŠ† On)
7776adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐡) β†’ π‘Œ βŠ† On)
7877sselda 3945 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐡) ∧ 𝑠 ∈ π‘Œ) β†’ 𝑠 ∈ On)
791ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐡) ∧ 𝑠 ∈ π‘Œ) β†’ 𝐴 ∈ On)
80 naddss2 8636 . . . . . . . . . . . 12 ((π‘ž ∈ On ∧ 𝑠 ∈ On ∧ 𝐴 ∈ On) β†’ (π‘ž βŠ† 𝑠 ↔ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
8169, 78, 79, 80syl3anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ π‘ž ∈ 𝐡) ∧ 𝑠 ∈ π‘Œ) β†’ (π‘ž βŠ† 𝑠 ↔ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
8281rexbidva 3174 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ 𝐡) β†’ (βˆƒπ‘  ∈ π‘Œ π‘ž βŠ† 𝑠 ↔ βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
8382ralbidva 3173 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ π‘ž βŠ† 𝑠 ↔ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
8465, 83mpbid 231 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠))
851snssd 4770 . . . . . . . . . . . 12 (πœ‘ β†’ {𝐴} βŠ† On)
86 xpss12 5649 . . . . . . . . . . . 12 (({𝐴} βŠ† On ∧ π‘Œ βŠ† On) β†’ ({𝐴} Γ— π‘Œ) βŠ† (On Γ— On))
8785, 76, 86syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ ({𝐴} Γ— π‘Œ) βŠ† (On Γ— On))
88 sseq2 3971 . . . . . . . . . . . 12 (𝑑 = (π‘Ÿ +no 𝑠) β†’ ((𝐴 +no π‘ž) βŠ† 𝑑 ↔ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
8988imaeqexov 7593 . . . . . . . . . . 11 (( +no Fn (On Γ— On) ∧ ({𝐴} Γ— π‘Œ) βŠ† (On Γ— On)) β†’ (βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
905, 87, 89sylancr 588 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
91 oveq1 7365 . . . . . . . . . . . . . 14 (π‘Ÿ = 𝐴 β†’ (π‘Ÿ +no 𝑠) = (𝐴 +no 𝑠))
9291sseq2d 3977 . . . . . . . . . . . . 13 (π‘Ÿ = 𝐴 β†’ ((𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
9392rexbidv 3176 . . . . . . . . . . . 12 (π‘Ÿ = 𝐴 β†’ (βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ π‘Œ (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
9493rexsng 4636 . . . . . . . . . . 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 867 . . . . . . . 8 (βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
10099ralimi 3087 . . . . . . 7 (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑 β†’ βˆ€π‘ž ∈ 𝐡 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
10198, 100syl 17 . . . . . 6 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
102 rexun 4151 . . . . . . 7 (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
103102ralbii 3097 . . . . . 6 (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑 ↔ βˆ€π‘ž ∈ 𝐡 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝐴 +no π‘ž) βŠ† 𝑑))
104101, 103sylibr 233 . . . . 5 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑)
105 xpss12 5649 . . . . . . . 8 (({𝐴} βŠ† On ∧ 𝐡 βŠ† On) β†’ ({𝐴} Γ— 𝐡) βŠ† (On Γ— On))
10685, 67, 105syl2anc 585 . . . . . . 7 (πœ‘ β†’ ({𝐴} Γ— 𝐡) βŠ† (On Γ— On))
107 sseq1 3970 . . . . . . . . 9 (𝑐 = (𝑝 +no π‘ž) β†’ (𝑐 βŠ† 𝑑 ↔ (𝑝 +no π‘ž) βŠ† 𝑑))
108107rexbidv 3176 . . . . . . . 8 (𝑐 = (𝑝 +no π‘ž) β†’ (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ↔ βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑))
109108imaeqalov 7594 . . . . . . 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 7365 . . . . . . . . . . 11 (𝑝 = 𝐴 β†’ (𝑝 +no π‘ž) = (𝐴 +no π‘ž))
112111sseq1d 3976 . . . . . . . . . 10 (𝑝 = 𝐴 β†’ ((𝑝 +no π‘ž) βŠ† 𝑑 ↔ (𝐴 +no π‘ž) βŠ† 𝑑))
113112rexbidv 3176 . . . . . . . . 9 (𝑝 = 𝐴 β†’ (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑))
114113ralbidv 3175 . . . . . . . 8 (𝑝 = 𝐴 β†’ (βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆ€π‘ž ∈ 𝐡 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝐴 +no π‘ž) βŠ† 𝑑))
115114ralsng 4635 . . . . . . 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 8621 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 𝑝 βŠ† π‘Ÿ)
120 onss 7720 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On β†’ 𝐴 βŠ† On)
1211, 120syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 βŠ† On)
122121sselda 3945 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ 𝑝 ∈ On)
123122adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝐴) ∧ π‘Ÿ ∈ 𝑋) β†’ 𝑝 ∈ On)
124 ssintub 4928 . . . . . . . . . . . . . . . 16 𝑋 βŠ† ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯}
12531, 121eqsstrrd 3984 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ∩ {π‘₯ ∈ On ∣ 𝑋 βŠ† π‘₯} βŠ† On)
126124, 125sstrid 3956 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 βŠ† On)
127126adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ 𝑋 βŠ† On)
128127sselda 3945 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝐴) ∧ π‘Ÿ ∈ 𝑋) β†’ π‘Ÿ ∈ On)
1292ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝐴) ∧ π‘Ÿ ∈ 𝑋) β†’ 𝐡 ∈ On)
130 naddss1 8635 . . . . . . . . . . . . 13 ((𝑝 ∈ On ∧ π‘Ÿ ∈ On ∧ 𝐡 ∈ On) β†’ (𝑝 βŠ† π‘Ÿ ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
131123, 128, 129, 130syl3anc 1372 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝐴) ∧ π‘Ÿ ∈ 𝑋) β†’ (𝑝 βŠ† π‘Ÿ ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
132131rexbidva 3174 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ (βˆƒπ‘Ÿ ∈ 𝑋 𝑝 βŠ† π‘Ÿ ↔ βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
133132ralbidva 3173 . . . . . . . . . 10 (πœ‘ β†’ (βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 𝑝 βŠ† π‘Ÿ ↔ βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
134119, 133mpbid 231 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 βˆƒπ‘Ÿ ∈ 𝑋 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡))
1352snssd 4770 . . . . . . . . . . . . 13 (πœ‘ β†’ {𝐡} βŠ† On)
136 xpss12 5649 . . . . . . . . . . . . 13 ((𝑋 βŠ† On ∧ {𝐡} βŠ† On) β†’ (𝑋 Γ— {𝐡}) βŠ† (On Γ— On))
137126, 135, 136syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑋 Γ— {𝐡}) βŠ† (On Γ— On))
138 sseq2 3971 . . . . . . . . . . . . 13 (𝑑 = (π‘Ÿ +no 𝑠) β†’ ((𝑝 +no 𝐡) βŠ† 𝑑 ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
139138imaeqexov 7593 . . . . . . . . . . . 12 (( +no Fn (On Γ— On) ∧ (𝑋 Γ— {𝐡}) βŠ† (On Γ— On)) β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ 𝑋 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
1405, 137, 139sylancr 588 . . . . . . . . . . 11 (πœ‘ β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ βˆƒπ‘Ÿ ∈ 𝑋 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
141 oveq2 7366 . . . . . . . . . . . . . . 15 (𝑠 = 𝐡 β†’ (π‘Ÿ +no 𝑠) = (π‘Ÿ +no 𝐡))
142141sseq2d 3977 . . . . . . . . . . . . . 14 (𝑠 = 𝐡 β†’ ((𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠) ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
143142rexsng 4636 . . . . . . . . . . . . 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 866 . . . . . . . . 9 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 β†’ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
150149ralimi 3087 . . . . . . . 8 (βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 β†’ βˆ€π‘ ∈ 𝐴 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
151148, 150syl 17 . . . . . . 7 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
152 rexun 4151 . . . . . . . 8 (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
153152ralbii 3097 . . . . . . 7 (βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑 ↔ βˆ€π‘ ∈ 𝐴 (βˆƒπ‘‘ ∈ ( +no β€œ (𝑋 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑑 ∨ βˆƒπ‘‘ ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))(𝑝 +no 𝐡) βŠ† 𝑑))
154151, 153sylibr 233 . . . . . 6 (πœ‘ β†’ βˆ€π‘ ∈ 𝐴 βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑)
155 oveq2 7366 . . . . . . . . . . 11 (π‘ž = 𝐡 β†’ (𝑝 +no π‘ž) = (𝑝 +no 𝐡))
156155sseq1d 3976 . . . . . . . . . 10 (π‘ž = 𝐡 β†’ ((𝑝 +no π‘ž) βŠ† 𝑑 ↔ (𝑝 +no 𝐡) βŠ† 𝑑))
157156rexbidv 3176 . . . . . . . . 9 (π‘ž = 𝐡 β†’ (βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no π‘ž) βŠ† 𝑑 ↔ βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))(𝑝 +no 𝐡) βŠ† 𝑑))
158157ralsng 4635 . . . . . . . 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 5649 . . . . . . 7 ((𝐴 βŠ† On ∧ {𝐡} βŠ† On) β†’ (𝐴 Γ— {𝐡}) βŠ† (On Γ— On))
163121, 135, 162syl2anc 585 . . . . . 6 (πœ‘ β†’ (𝐴 Γ— {𝐡}) βŠ† (On Γ— On))
164108imaeqalov 7594 . . . . . 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 4152 . . . 4 (βˆ€π‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ↔ (βˆ€π‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑 ∧ βˆ€π‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑))
168118, 166, 167sylanbrc 584 . . 3 (πœ‘ β†’ βˆ€π‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))βˆƒπ‘‘ ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))𝑐 βŠ† 𝑑)
169124, 31sseqtrrid 3998 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 βŠ† 𝐴)
170169sselda 3945 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ 𝑝 ∈ 𝐴)
171 ssid 3967 . . . . . . . . . . 11 𝑝 βŠ† 𝑝
172 sseq2 3971 . . . . . . . . . . . 12 (π‘Ÿ = 𝑝 β†’ (𝑝 βŠ† π‘Ÿ ↔ 𝑝 βŠ† 𝑝))
173172rspcev 3582 . . . . . . . . . . 11 ((𝑝 ∈ 𝐴 ∧ 𝑝 βŠ† 𝑝) β†’ βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ)
174170, 171, 173sylancl 587 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ)
175174ralrimiva 3144 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ)
176126sselda 3945 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ 𝑝 ∈ On)
177176adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑋) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝑝 ∈ On)
178121adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ 𝐴 βŠ† On)
179178sselda 3945 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑋) ∧ π‘Ÿ ∈ 𝐴) β†’ π‘Ÿ ∈ On)
1802ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑋) ∧ π‘Ÿ ∈ 𝐴) β†’ 𝐡 ∈ On)
181177, 179, 180, 130syl3anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ 𝑋) ∧ π‘Ÿ ∈ 𝐴) β†’ (𝑝 βŠ† π‘Ÿ ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
182181rexbidva 3174 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ 𝑋) β†’ (βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ ↔ βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
183182ralbidva 3173 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 𝑝 βŠ† π‘Ÿ ↔ βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡)))
184175, 183mpbid 231 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ ∈ 𝑋 βˆƒπ‘Ÿ ∈ 𝐴 (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝐡))
185 sseq2 3971 . . . . . . . . . . . 12 (𝑏 = (π‘Ÿ +no 𝑠) β†’ ((𝑝 +no 𝐡) βŠ† 𝑏 ↔ (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
186185imaeqexov 7593 . . . . . . . . . . 11 (( +no Fn (On Γ— On) ∧ (𝐴 Γ— {𝐡}) βŠ† (On Γ— On)) β†’ (βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 ↔ βˆƒπ‘Ÿ ∈ 𝐴 βˆƒπ‘  ∈ {𝐡} (𝑝 +no 𝐡) βŠ† (π‘Ÿ +no 𝑠)))
1875, 163, 186sylancr 588 . . . . . . . . . 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 867 . . . . . . . 8 (βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 β†’ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏))
193192ralimi 3087 . . . . . . 7 (βˆ€π‘ ∈ 𝑋 βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏 β†’ βˆ€π‘ ∈ 𝑋 (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏))
194191, 193syl 17 . . . . . 6 (πœ‘ β†’ βˆ€π‘ ∈ 𝑋 (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝑝 +no 𝐡) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝑝 +no 𝐡) βŠ† 𝑏))
195155sseq1d 3976 . . . . . . . . . . . 12 (π‘ž = 𝐡 β†’ ((𝑝 +no π‘ž) βŠ† 𝑏 ↔ (𝑝 +no 𝐡) βŠ† 𝑏))
196195rexbidv 3176 . . . . . . . . . . 11 (π‘ž = 𝐡 β†’ (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏 ↔ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no 𝐡) βŠ† 𝑏))
197196ralsng 4635 . . . . . . . . . 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 4151 . . . . . . . 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 3970 . . . . . . . 8 (π‘Ž = (𝑝 +no π‘ž) β†’ (π‘Ž βŠ† 𝑏 ↔ (𝑝 +no π‘ž) βŠ† 𝑏))
205204rexbidv 3176 . . . . . . 7 (π‘Ž = (𝑝 +no π‘ž) β†’ (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ↔ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏))
206205imaeqalov 7594 . . . . . 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 4928 . . . . . . . . . . . . 13 π‘Œ βŠ† ∩ {𝑦 ∈ On ∣ π‘Œ βŠ† 𝑦}
210209, 47sseqtrrid 3998 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ βŠ† 𝐡)
211210sselda 3945 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ π‘ž ∈ 𝐡)
212 ssid 3967 . . . . . . . . . . 11 π‘ž βŠ† π‘ž
213 sseq2 3971 . . . . . . . . . . . 12 (𝑠 = π‘ž β†’ (π‘ž βŠ† 𝑠 ↔ π‘ž βŠ† π‘ž))
214213rspcev 3582 . . . . . . . . . . 11 ((π‘ž ∈ 𝐡 ∧ π‘ž βŠ† π‘ž) β†’ βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠)
215211, 212, 214sylancl 587 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠)
216215ralrimiva 3144 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘ž ∈ π‘Œ βˆƒπ‘  ∈ 𝐡 π‘ž βŠ† 𝑠)
21792rexbidv 3176 . . . . . . . . . . . . . 14 (π‘Ÿ = 𝐴 β†’ (βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
218217rexsng 4636 . . . . . . . . . . . . 13 (𝐴 ∈ On β†’ (βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
2191, 218syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
220219adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ (βˆƒπ‘Ÿ ∈ {𝐴}βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠) ↔ βˆƒπ‘  ∈ 𝐡 (𝐴 +no π‘ž) βŠ† (𝐴 +no 𝑠)))
221 sseq2 3971 . . . . . . . . . . . . . 14 (𝑏 = (π‘Ÿ +no 𝑠) β†’ ((𝐴 +no π‘ž) βŠ† 𝑏 ↔ (𝐴 +no π‘ž) βŠ† (π‘Ÿ +no 𝑠)))
222221imaeqexov 7593 . . . . . . . . . . . . 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 3945 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ π‘ž ∈ On)
226225adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘ž ∈ π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ π‘ž ∈ On)
22767adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘ž ∈ π‘Œ) β†’ 𝐡 βŠ† On)
228227sselda 3945 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘ž ∈ π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ 𝑠 ∈ On)
2291ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘ž ∈ π‘Œ) ∧ 𝑠 ∈ 𝐡) β†’ 𝐴 ∈ On)
230226, 228, 229, 80syl3anc 1372 . . . . . . . . . . . 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 866 . . . . . . . . 9 (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 β†’ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
236235ralimi 3087 . . . . . . . 8 (βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 β†’ βˆ€π‘ž ∈ π‘Œ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
237234, 236syl 17 . . . . . . 7 (πœ‘ β†’ βˆ€π‘ž ∈ π‘Œ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
238 rexun 4151 . . . . . . . 8 (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
239238ralbii 3097 . . . . . . 7 (βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏 ↔ βˆ€π‘ž ∈ π‘Œ (βˆƒπ‘ ∈ ( +no β€œ ({𝐴} Γ— 𝐡))(𝐴 +no π‘ž) βŠ† 𝑏 ∨ βˆƒπ‘ ∈ ( +no β€œ (𝐴 Γ— {𝐡}))(𝐴 +no π‘ž) βŠ† 𝑏))
240237, 239sylibr 233 . . . . . 6 (πœ‘ β†’ βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏)
241111sseq1d 3976 . . . . . . . . . 10 (𝑝 = 𝐴 β†’ ((𝑝 +no π‘ž) βŠ† 𝑏 ↔ (𝐴 +no π‘ž) βŠ† 𝑏))
242241rexbidv 3176 . . . . . . . . 9 (𝑝 = 𝐴 β†’ (βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏 ↔ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏))
243242ralbidv 3175 . . . . . . . 8 (𝑝 = 𝐴 β†’ (βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝑝 +no π‘ž) βŠ† 𝑏 ↔ βˆ€π‘ž ∈ π‘Œ βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))(𝐴 +no π‘ž) βŠ† 𝑏))
244243ralsng 4635 . . . . . . 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 7594 . . . . . 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 4152 . . . 4 (βˆ€π‘Ž ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ↔ (βˆ€π‘Ž ∈ ( +no β€œ (𝑋 Γ— {𝐡}))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏 ∧ βˆ€π‘Ž ∈ ( +no β€œ ({𝐴} Γ— π‘Œ))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏))
251208, 249, 250sylanbrc 584 . . 3 (πœ‘ β†’ βˆ€π‘Ž ∈ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ)))βˆƒπ‘ ∈ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡})))π‘Ž βŠ† 𝑏)
25230, 64, 168, 251cofon2 8620 . 2 (πœ‘ β†’ ∩ {𝑀 ∈ On ∣ (( +no β€œ ({𝐴} Γ— 𝐡)) βˆͺ ( +no β€œ (𝐴 Γ— {𝐡}))) βŠ† 𝑀} = ∩ {𝑧 ∈ On ∣ (( +no β€œ (𝑋 Γ— {𝐡})) βˆͺ ( +no β€œ ({𝐴} Γ— π‘Œ))) βŠ† 𝑧})
2534, 252eqtrd 2777 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 3065  βˆƒwrex 3074  {crab 3408  Vcvv 3446   βˆͺ cun 3909   βŠ† wss 3911  π’« cpw 4561  {csn 4587  βˆ© cint 4908   Γ— cxp 5632  ran crn 5635   β€œ cima 5637  Oncon0 6318  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  (class class class)co 7358   +no cnadd 8612
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 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-frecs 8213  df-nadd 8613
This theorem is referenced by:  naddasslem1  8639  naddasslem2  8640
  Copyright terms: Public domain W3C validator