Step | Hyp | Ref
| Expression |
1 | | naddov 33583 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no
“ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}) |
2 | | snssi 4730 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → {𝐴} ⊆ On) |
3 | | onss 7577 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) |
4 | | xpss12 5575 |
. . . . . . . . 9
⊢ (({𝐴} ⊆ On ∧ 𝐵 ⊆ On) → ({𝐴} × 𝐵) ⊆ (On × On)) |
5 | 2, 3, 4 | syl2an 599 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ({𝐴} × 𝐵) ⊆ (On × On)) |
6 | | naddfn 33580 |
. . . . . . . . 9
⊢ +no Fn
(On × On) |
7 | 6 | fndmi 6491 |
. . . . . . . 8
⊢ dom +no =
(On × On) |
8 | 5, 7 | sseqtrrdi 3961 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ({𝐴} × 𝐵) ⊆ dom +no ) |
9 | | fnfun 6488 |
. . . . . . . . 9
⊢ ( +no Fn
(On × On) → Fun +no ) |
10 | 6, 9 | ax-mp 5 |
. . . . . . . 8
⊢ Fun
+no |
11 | | funimassov 7394 |
. . . . . . . 8
⊢ ((Fun +no
∧ ({𝐴} × 𝐵) ⊆ dom +no ) → ((
+no “ ({𝐴} ×
𝐵)) ⊆ 𝑥 ↔ ∀𝑡 ∈ {𝐴}∀𝑦 ∈ 𝐵 (𝑡 +no 𝑦) ∈ 𝑥)) |
12 | 10, 11 | mpan 690 |
. . . . . . 7
⊢ (({𝐴} × 𝐵) ⊆ dom +no → (( +no “
({𝐴} × 𝐵)) ⊆ 𝑥 ↔ ∀𝑡 ∈ {𝐴}∀𝑦 ∈ 𝐵 (𝑡 +no 𝑦) ∈ 𝑥)) |
13 | 8, 12 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (( +no
“ ({𝐴} × 𝐵)) ⊆ 𝑥 ↔ ∀𝑡 ∈ {𝐴}∀𝑦 ∈ 𝐵 (𝑡 +no 𝑦) ∈ 𝑥)) |
14 | | oveq1 7229 |
. . . . . . . . . 10
⊢ (𝑡 = 𝐴 → (𝑡 +no 𝑦) = (𝐴 +no 𝑦)) |
15 | 14 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑡 = 𝐴 → ((𝑡 +no 𝑦) ∈ 𝑥 ↔ (𝐴 +no 𝑦) ∈ 𝑥)) |
16 | 15 | ralbidv 3119 |
. . . . . . . 8
⊢ (𝑡 = 𝐴 → (∀𝑦 ∈ 𝐵 (𝑡 +no 𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥)) |
17 | 16 | ralsng 4598 |
. . . . . . 7
⊢ (𝐴 ∈ On → (∀𝑡 ∈ {𝐴}∀𝑦 ∈ 𝐵 (𝑡 +no 𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥)) |
18 | 17 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑡 ∈ {𝐴}∀𝑦 ∈ 𝐵 (𝑡 +no 𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥)) |
19 | 13, 18 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (( +no
“ ({𝐴} × 𝐵)) ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥)) |
20 | | onss 7577 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
21 | | snssi 4730 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → {𝐵} ⊆ On) |
22 | | xpss12 5575 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ {𝐵} ⊆ On) → (𝐴 × {𝐵}) ⊆ (On × On)) |
23 | 20, 21, 22 | syl2an 599 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 × {𝐵}) ⊆ (On × On)) |
24 | 23, 7 | sseqtrrdi 3961 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 × {𝐵}) ⊆ dom +no ) |
25 | | funimassov 7394 |
. . . . . . . 8
⊢ ((Fun +no
∧ (𝐴 × {𝐵}) ⊆ dom +no ) → ((
+no “ (𝐴 ×
{𝐵})) ⊆ 𝑥 ↔ ∀𝑧 ∈ 𝐴 ∀𝑡 ∈ {𝐵} (𝑧 +no 𝑡) ∈ 𝑥)) |
26 | 10, 25 | mpan 690 |
. . . . . . 7
⊢ ((𝐴 × {𝐵}) ⊆ dom +no → (( +no “
(𝐴 × {𝐵})) ⊆ 𝑥 ↔ ∀𝑧 ∈ 𝐴 ∀𝑡 ∈ {𝐵} (𝑧 +no 𝑡) ∈ 𝑥)) |
27 | 24, 26 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (( +no
“ (𝐴 × {𝐵})) ⊆ 𝑥 ↔ ∀𝑧 ∈ 𝐴 ∀𝑡 ∈ {𝐵} (𝑧 +no 𝑡) ∈ 𝑥)) |
28 | | oveq2 7230 |
. . . . . . . . . 10
⊢ (𝑡 = 𝐵 → (𝑧 +no 𝑡) = (𝑧 +no 𝐵)) |
29 | 28 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑡 = 𝐵 → ((𝑧 +no 𝑡) ∈ 𝑥 ↔ (𝑧 +no 𝐵) ∈ 𝑥)) |
30 | 29 | ralsng 4598 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (∀𝑡 ∈ {𝐵} (𝑧 +no 𝑡) ∈ 𝑥 ↔ (𝑧 +no 𝐵) ∈ 𝑥)) |
31 | 30 | ralbidv 3119 |
. . . . . . 7
⊢ (𝐵 ∈ On → (∀𝑧 ∈ 𝐴 ∀𝑡 ∈ {𝐵} (𝑧 +no 𝑡) ∈ 𝑥 ↔ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)) |
32 | 31 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑧 ∈ 𝐴 ∀𝑡 ∈ {𝐵} (𝑧 +no 𝑡) ∈ 𝑥 ↔ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)) |
33 | 27, 32 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (( +no
“ (𝐴 × {𝐵})) ⊆ 𝑥 ↔ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)) |
34 | 19, 33 | anbi12d 634 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((( +no
“ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥) ↔ (∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥 ∧ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥))) |
35 | 34 | rabbidv 3397 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∈ On ∣ (( +no
“ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥 ∧ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)}) |
36 | 35 | inteqd 4873 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∩ {𝑥
∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣
(∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥 ∧ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)}) |
37 | 1, 36 | eqtrd 2778 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣
(∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥 ∧ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)}) |