Step | Hyp | Ref
| Expression |
1 | | eloni 5650 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → Ord 𝐵) |
2 | 1 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → Ord 𝐵) |
3 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ 𝐵) |
4 | | ordsucss 6910 |
. . . . . . . 8
⊢ (Ord
𝐵 → (𝑥 ∈ 𝐵 → suc 𝑥 ⊆ 𝐵)) |
5 | 2, 3, 4 | sylc 63 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → suc 𝑥 ⊆ 𝐵) |
6 | | onelon 5665 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
7 | 6 | ad2ant2lr 780 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ On) |
8 | | suceloni 6905 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → suc 𝑥 ∈ On) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → suc 𝑥 ∈ On) |
10 | | simplr 788 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝐵 ∈ On) |
11 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝐴 ∈ On) |
12 | | omwordi 7538 |
. . . . . . . 8
⊢ ((suc
𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) → (suc 𝑥 ⊆ 𝐵 → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵))) |
13 | 9, 10, 11, 12 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (suc 𝑥 ⊆ 𝐵 → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵))) |
14 | 5, 13 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵)) |
15 | | simprr 792 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
16 | | onelon 5665 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
17 | 16 | ad2ant2rl 781 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ On) |
18 | | omcl 7503 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
𝑥) ∈
On) |
19 | 11, 7, 18 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·𝑜 𝑥) ∈ On) |
20 | | oaord 7514 |
. . . . . . . . 9
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜
𝑥) ∈ On) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
21 | 17, 11, 19, 20 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
22 | 15, 21 | mpbid 221 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |
23 | | omsuc 7493 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
suc 𝑥) = ((𝐴 ·𝑜
𝑥) +𝑜
𝐴)) |
24 | 11, 7, 23 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |
25 | 22, 24 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 suc 𝑥)) |
26 | 14, 25 | sseldd 3569 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) |
27 | 26 | ralrimivva 2954 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) |
28 | | omxpenlem.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) |
29 | 28 | fmpt2 7126 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ↔ 𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵)) |
30 | 27, 29 | sylib 207 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵)) |
31 | | ffn 5958 |
. . 3
⊢ (𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵) → 𝐹 Fn (𝐵 × 𝐴)) |
32 | 30, 31 | syl 17 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹 Fn (𝐵 × 𝐴)) |
33 | | simpll 786 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝐴 ∈ On) |
34 | | omcl 7503 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) ∈
On) |
35 | | onelon 5665 |
. . . . . . . 8
⊢ (((𝐴 ·𝑜
𝐵) ∈ On ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝑚 ∈ On) |
36 | 34, 35 | sylan 487 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝑚 ∈ On) |
37 | | noel 3878 |
. . . . . . . . . . . 12
⊢ ¬
𝑚 ∈
∅ |
38 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) = (∅
·𝑜 𝐵)) |
39 | | om0r 7506 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
·𝑜 𝐵) = ∅) |
40 | 38, 39 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ·𝑜
𝐵) =
∅) |
41 | 40 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) ↔ 𝑚 ∈ ∅)) |
42 | 37, 41 | mtbiri 316 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → ¬ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) |
43 | 42 | ex 449 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → (𝐴 = ∅ → ¬ 𝑚 ∈ (𝐴 ·𝑜 𝐵))) |
44 | 43 | necon2ad 2797 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (𝑚 ∈ (𝐴 ·𝑜 𝐵) → 𝐴 ≠ ∅)) |
45 | 44 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) → 𝐴 ≠ ∅)) |
46 | 45 | imp 444 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝐴 ≠ ∅) |
47 | | omeu 7552 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑚 ∈ On ∧ 𝐴 ≠ ∅) →
∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) |
48 | 33, 36, 46, 47 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) |
49 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑚 ∈ V |
50 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑛 ∈ V |
51 | 49, 50 | brcnv 5227 |
. . . . . . . 8
⊢ (𝑚◡𝐹𝑛 ↔ 𝑛𝐹𝑚) |
52 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵))) |
53 | 52 | biimpac 502 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) |
54 | 6 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ On → (𝑥 ∈ 𝐵 → 𝑥 ∈ On)) |
55 | 54 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝐵 → 𝑥 ∈ On)) |
56 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
57 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑥 ∈ On) |
58 | 56, 57, 18 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ On) |
59 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑦 ∈ 𝐴) |
60 | 56, 59, 16 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑦 ∈ On) |
61 | | oaword1 7519 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ·𝑜
𝑥) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
𝑥) ⊆ ((𝐴 ·𝑜
𝑥) +𝑜
𝑦)) |
62 | 58, 60, 61 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) |
63 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) |
64 | 34 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝐵) ∈ On) |
65 | | ontr2 5689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ·𝑜
𝑥) ∈ On ∧ (𝐴 ·𝑜
𝐵) ∈ On) →
(((𝐴
·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))) |
66 | 58, 64, 65 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (((𝐴 ·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))) |
67 | 62, 63, 66 | mp2and 711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵)) |
68 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝐵 ∈ On) |
69 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) → (𝐴 ·𝑜
𝐵) ≠
∅) |
70 | 63, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝐵) ≠ ∅) |
71 | | on0eln0 5697 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ·𝑜
𝐵) ∈ On →
(∅ ∈ (𝐴
·𝑜 𝐵) ↔ (𝐴 ·𝑜 𝐵) ≠
∅)) |
72 | 64, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·𝑜
𝐵) ↔ (𝐴 ·𝑜
𝐵) ≠
∅)) |
73 | 70, 72 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ∅ ∈ (𝐴 ·𝑜
𝐵)) |
74 | | om00el 7543 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ (𝐴
·𝑜 𝐵) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵))) |
75 | 74 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·𝑜
𝐵) ↔ (∅ ∈
𝐴 ∧ ∅ ∈
𝐵))) |
76 | 73, 75 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵)) |
77 | 76 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ∅ ∈ 𝐴) |
78 | | omord2 7534 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑥 ∈ 𝐵 ↔ (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))) |
79 | 57, 68, 56, 77, 78 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝑥 ∈ 𝐵 ↔ (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))) |
80 | 67, 79 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑥 ∈ 𝐵) |
81 | 80 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ On → 𝑥 ∈ 𝐵)) |
82 | 55, 81 | impbid 201 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ On)) |
83 | 82 | expr 641 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵)) → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ On))) |
84 | 83 | pm5.32rd 670 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ((𝐴 ·𝑜
𝑥) +𝑜
𝑦) ∈ (𝐴 ·𝑜
𝐵)) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴))) |
85 | 53, 84 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑚 ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴))) |
86 | 85 | expr 641 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴)))) |
87 | 86 | pm5.32rd 670 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))) |
88 | | eqcom 2617 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚) |
89 | 88 | anbi2i 726 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) |
90 | 87, 89 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
91 | 90 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))) |
92 | | an12 834 |
. . . . . . . . . . 11
⊢ ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
93 | 91, 92 | syl6bb 275 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))) |
94 | 93 | 2exbidv 1839 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))) |
95 | | df-mpt2 6554 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) = {〈〈𝑥, 𝑦〉, 𝑚〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))} |
96 | | dfoprab2 6599 |
. . . . . . . . . . . 12
⊢
{〈〈𝑥,
𝑦〉, 𝑚〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))} = {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))} |
97 | 28, 95, 96 | 3eqtri 2636 |
. . . . . . . . . . 11
⊢ 𝐹 = {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))} |
98 | 97 | breqi 4589 |
. . . . . . . . . 10
⊢ (𝑛𝐹𝑚 ↔ 𝑛{〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}𝑚) |
99 | | df-br 4584 |
. . . . . . . . . 10
⊢ (𝑛{〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}𝑚 ↔ 〈𝑛, 𝑚〉 ∈ {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}) |
100 | | opabid 4907 |
. . . . . . . . . 10
⊢
(〈𝑛, 𝑚〉 ∈ {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))} ↔ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))) |
101 | 98, 99, 100 | 3bitri 285 |
. . . . . . . . 9
⊢ (𝑛𝐹𝑚 ↔ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))) |
102 | | r2ex 3043 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
103 | 94, 101, 102 | 3bitr4g 302 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑛𝐹𝑚 ↔ ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
104 | 51, 103 | syl5bb 271 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑚◡𝐹𝑛 ↔ ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
105 | 104 | eubidv 2478 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (∃!𝑛 𝑚◡𝐹𝑛 ↔ ∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))) |
106 | 48, 105 | mpbird 246 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ∃!𝑛 𝑚◡𝐹𝑛) |
107 | 106 | ralrimiva 2949 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑚 ∈ (𝐴 ·𝑜 𝐵)∃!𝑛 𝑚◡𝐹𝑛) |
108 | | fnres 5921 |
. . . 4
⊢ ((◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵) ↔ ∀𝑚 ∈ (𝐴 ·𝑜 𝐵)∃!𝑛 𝑚◡𝐹𝑛) |
109 | 107, 108 | sylibr 223 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵)) |
110 | | relcnv 5422 |
. . . . 5
⊢ Rel ◡𝐹 |
111 | | df-rn 5049 |
. . . . . 6
⊢ ran 𝐹 = dom ◡𝐹 |
112 | | frn 5966 |
. . . . . . 7
⊢ (𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵) → ran 𝐹 ⊆ (𝐴 ·𝑜 𝐵)) |
113 | 30, 112 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ran 𝐹 ⊆ (𝐴 ·𝑜 𝐵)) |
114 | 111, 113 | syl5eqssr 3613 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → dom ◡𝐹 ⊆ (𝐴 ·𝑜 𝐵)) |
115 | | relssres 5357 |
. . . . 5
⊢ ((Rel
◡𝐹 ∧ dom ◡𝐹 ⊆ (𝐴 ·𝑜 𝐵)) → (◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) = ◡𝐹) |
116 | 110, 114,
115 | sylancr 694 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) = ◡𝐹) |
117 | 116 | fneq1d 5895 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((◡𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵) ↔ ◡𝐹 Fn (𝐴 ·𝑜 𝐵))) |
118 | 109, 117 | mpbid 221 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ◡𝐹 Fn (𝐴 ·𝑜 𝐵)) |
119 | | dff1o4 6058 |
. 2
⊢ (𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·𝑜 𝐵) ↔ (𝐹 Fn (𝐵 × 𝐴) ∧ ◡𝐹 Fn (𝐴 ·𝑜 𝐵))) |
120 | 32, 118, 119 | sylanbrc 695 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·𝑜 𝐵)) |