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