Step | Hyp | Ref
| Expression |
1 | | eloni 5733 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → Ord 𝐵) |
2 | 1 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → Ord 𝐵) |
3 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ 𝐵) |
4 | | ordsucss 7018 |
. . . . . . . 8
⊢ (Ord
𝐵 → (𝑥 ∈ 𝐵 → suc 𝑥 ⊆ 𝐵)) |
5 | 2, 3, 4 | sylc 65 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → suc 𝑥 ⊆ 𝐵) |
6 | | onelon 5748 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
7 | 6 | ad2ant2lr 784 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ On) |
8 | | suceloni 7013 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → suc 𝑥 ∈ On) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → suc 𝑥 ∈ On) |
10 | | simplr 792 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝐵 ∈ On) |
11 | | simpll 790 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝐴 ∈ On) |
12 | | omwordi 7651 |
. . . . . . . 8
⊢ ((suc
𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) → (suc 𝑥 ⊆ 𝐵 → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵))) |
13 | 9, 10, 11, 12 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (suc 𝑥 ⊆ 𝐵 → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵))) |
14 | 5, 13 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵)) |
15 | | simprr 796 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
16 | | onelon 5748 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
17 | 16 | ad2ant2rl 785 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ On) |
18 | | omcl 7616 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
𝑥) ∈
On) |
19 | 11, 7, 18 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·𝑜 𝑥) ∈ On) |
20 | | oaord 7627 |
. . . . . . . . 9
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜
𝑥) ∈ On) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
21 | 17, 11, 19, 20 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
22 | 15, 21 | mpbid 222 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |
23 | | omsuc 7606 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
suc 𝑥) = ((𝐴 ·𝑜
𝑥) +𝑜
𝐴)) |
24 | 11, 7, 23 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |
25 | 22, 24 | eleqtrrd 2704 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 suc 𝑥)) |
26 | 14, 25 | sseldd 3604 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) |
27 | 26 | ralrimivva 2971 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) |
28 | | omxpenlem.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) |
29 | 28 | fmpt2 7237 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ↔ 𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵)) |
30 | 27, 29 | sylib 208 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵)) |
31 | | ffn 6045 |
. . 3
⊢ (𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵) → 𝐹 Fn (𝐵 × 𝐴)) |
32 | 30, 31 | syl 17 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹 Fn (𝐵 × 𝐴)) |
33 | | simpll 790 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝐴 ∈ On) |
34 | | omcl 7616 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) ∈
On) |
35 | | onelon 5748 |
. . . . . . . 8
⊢ (((𝐴 ·𝑜
𝐵) ∈ On ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝑚 ∈ On) |
36 | 34, 35 | sylan 488 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝑚 ∈ On) |
37 | | noel 3919 |
. . . . . . . . . . . 12
⊢ ¬
𝑚 ∈
∅ |
38 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) = (∅
·𝑜 𝐵)) |
39 | | om0r 7619 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
·𝑜 𝐵) = ∅) |
40 | 38, 39 | sylan9eqr 2678 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ·𝑜
𝐵) =
∅) |
41 | 40 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) ↔ 𝑚 ∈ ∅)) |
42 | 37, 41 | mtbiri 317 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → ¬ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) |
43 | 42 | ex 450 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → (𝐴 = ∅ → ¬ 𝑚 ∈ (𝐴 ·𝑜 𝐵))) |
44 | 43 | necon2ad 2809 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (𝑚 ∈ (𝐴 ·𝑜 𝐵) → 𝐴 ≠ ∅)) |
45 | 44 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) → 𝐴 ≠ ∅)) |
46 | 45 | imp 445 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝐴 ≠ ∅) |
47 | | omeu 7665 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑚 ∈ On ∧ 𝐴 ≠ ∅) →
∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) |
48 | 33, 36, 46, 47 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) |
49 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑚 ∈ V |
50 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑛 ∈ V |
51 | 49, 50 | brcnv 5305 |
. . . . . . . 8
⊢ (𝑚◡𝐹𝑛 ↔ 𝑛𝐹𝑚) |
52 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵))) |
53 | 52 | biimpac 503 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) |
54 | 6 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ On → (𝑥 ∈ 𝐵 → 𝑥 ∈ On)) |
55 | 54 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝐵 → 𝑥 ∈ On)) |
56 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
57 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑥 ∈ On) |
58 | 56, 57, 18 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ On) |
59 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑦 ∈ 𝐴) |
60 | 56, 59, 16 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑦 ∈ On) |
61 | | oaword1 7632 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ·𝑜
𝑥) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
𝑥) ⊆ ((𝐴 ·𝑜
𝑥) +𝑜
𝑦)) |
62 | 58, 60, 61 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) |
63 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) |
64 | 34 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝐵) ∈ On) |
65 | | ontr2 5772 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ·𝑜
𝑥) ∈ On ∧ (𝐴 ·𝑜
𝐵) ∈ On) →
(((𝐴
·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))) |
66 | 58, 64, 65 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (((𝐴 ·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))) |
67 | 62, 63, 66 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵)) |
68 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝐵 ∈ On) |
69 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) → (𝐴 ·𝑜
𝐵) ≠
∅) |
70 | 63, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝐵) ≠ ∅) |
71 | | on0eln0 5780 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ·𝑜
𝐵) ∈ On →
(∅ ∈ (𝐴
·𝑜 𝐵) ↔ (𝐴 ·𝑜 𝐵) ≠
∅)) |
72 | 64, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·𝑜
𝐵) ↔ (𝐴 ·𝑜
𝐵) ≠
∅)) |
73 | 70, 72 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ∅ ∈ (𝐴 ·𝑜
𝐵)) |
74 | | om00el 7656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ (𝐴
·𝑜 𝐵) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵))) |
75 | 74 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·𝑜
𝐵) ↔ (∅ ∈
𝐴 ∧ ∅ ∈
𝐵))) |
76 | 73, 75 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵)) |
77 | 76 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ∅ ∈ 𝐴) |
78 | | omord2 7647 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑥 ∈ 𝐵 ↔ (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))) |
79 | 57, 68, 56, 77, 78 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝑥 ∈ 𝐵 ↔ (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))) |
80 | 67, 79 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑥 ∈ 𝐵) |
81 | 80 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ On → 𝑥 ∈ 𝐵)) |
82 | 55, 81 | impbid 202 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ On)) |
83 | 82 | expr 643 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵)) → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ On))) |
84 | 83 | pm5.32rd 672 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵)) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴))) |
85 | 53, 84 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑚 ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴))) |
86 | 85 | expr 643 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴)))) |
87 | 86 | pm5.32rd 672 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))) |
88 | | eqcom 2629 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚) |
89 | 88 | anbi2i 730 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) |
90 | 87, 89 | syl6bb 276 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
91 | 90 | anbi2d 740 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))) |
92 | | an12 838 |
. . . . . . . . . . 11
⊢ ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
93 | 91, 92 | syl6bb 276 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))) |
94 | 93 | 2exbidv 1852 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))) |
95 | | df-mpt2 6655 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) = {〈〈𝑥, 𝑦〉, 𝑚〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))} |
96 | | dfoprab2 6701 |
. . . . . . . . . . . 12
⊢
{〈〈𝑥,
𝑦〉, 𝑚〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))} = {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))} |
97 | 28, 95, 96 | 3eqtri 2648 |
. . . . . . . . . . 11
⊢ 𝐹 = {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))} |
98 | 97 | breqi 4659 |
. . . . . . . . . 10
⊢ (𝑛𝐹𝑚 ↔ 𝑛{〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}𝑚) |
99 | | df-br 4654 |
. . . . . . . . . 10
⊢ (𝑛{〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}𝑚 ↔ 〈𝑛, 𝑚〉 ∈ {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}) |
100 | | opabid 4982 |
. . . . . . . . . 10
⊢
(〈𝑛, 𝑚〉 ∈ {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))} ↔ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))) |
101 | 98, 99, 100 | 3bitri 286 |
. . . . . . . . 9
⊢ (𝑛𝐹𝑚 ↔ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))) |
102 | | r2ex 3061 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
103 | 94, 101, 102 | 3bitr4g 303 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑛𝐹𝑚 ↔ ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
104 | 51, 103 | syl5bb 272 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑚◡𝐹𝑛 ↔ ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
105 | 104 | eubidv 2490 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (∃!𝑛 𝑚◡𝐹𝑛 ↔ ∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
106 | 48, 105 | mpbird 247 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ∃!𝑛 𝑚◡𝐹𝑛) |
107 | 106 | ralrimiva 2966 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑚 ∈ (𝐴 ·𝑜 𝐵)∃!𝑛 𝑚◡𝐹𝑛) |
108 | | fnres 6007 |
. . . 4
⊢ ((◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵) ↔ ∀𝑚 ∈ (𝐴 ·𝑜 𝐵)∃!𝑛 𝑚◡𝐹𝑛) |
109 | 107, 108 | sylibr 224 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵)) |
110 | | relcnv 5503 |
. . . . 5
⊢ Rel ◡𝐹 |
111 | | df-rn 5125 |
. . . . . 6
⊢ ran 𝐹 = dom ◡𝐹 |
112 | | frn 6053 |
. . . . . . 7
⊢ (𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵) → ran 𝐹 ⊆ (𝐴 ·𝑜 𝐵)) |
113 | 30, 112 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ran 𝐹 ⊆ (𝐴 ·𝑜 𝐵)) |
114 | 111, 113 | syl5eqssr 3650 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → dom ◡𝐹 ⊆ (𝐴 ·𝑜 𝐵)) |
115 | | relssres 5437 |
. . . . 5
⊢ ((Rel
◡𝐹 ∧ dom ◡𝐹 ⊆ (𝐴 ·𝑜 𝐵)) → (◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) = ◡𝐹) |
116 | 110, 114,
115 | sylancr 695 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) = ◡𝐹) |
117 | 116 | fneq1d 5981 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵) ↔ ◡𝐹 Fn (𝐴 ·𝑜 𝐵))) |
118 | 109, 117 | mpbid 222 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ◡𝐹 Fn (𝐴 ·𝑜 𝐵)) |
119 | | dff1o4 6145 |
. 2
⊢ (𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·𝑜 𝐵) ↔ (𝐹 Fn (𝐵 × 𝐴) ∧ ◡𝐹 Fn (𝐴 ·𝑜 𝐵))) |
120 | 32, 118, 119 | sylanbrc 698 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·𝑜 𝐵)) |