| Step | Hyp | Ref
| Expression |
| 1 | | eloni 6394 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → Ord 𝐵) |
| 2 | 1 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → Ord 𝐵) |
| 3 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ 𝐵) |
| 4 | | ordsucss 7838 |
. . . . . . . 8
⊢ (Ord
𝐵 → (𝑥 ∈ 𝐵 → suc 𝑥 ⊆ 𝐵)) |
| 5 | 2, 3, 4 | sylc 65 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → suc 𝑥 ⊆ 𝐵) |
| 6 | | onelon 6409 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
| 7 | 6 | ad2ant2lr 748 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ On) |
| 8 | | onsuc 7831 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → suc 𝑥 ∈ On) |
| 9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → suc 𝑥 ∈ On) |
| 10 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝐵 ∈ On) |
| 11 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝐴 ∈ On) |
| 12 | | omwordi 8609 |
. . . . . . . 8
⊢ ((suc
𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) → (suc 𝑥 ⊆ 𝐵 → (𝐴 ·o suc 𝑥) ⊆ (𝐴 ·o 𝐵))) |
| 13 | 9, 10, 11, 12 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (suc 𝑥 ⊆ 𝐵 → (𝐴 ·o suc 𝑥) ⊆ (𝐴 ·o 𝐵))) |
| 14 | 5, 13 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·o suc 𝑥) ⊆ (𝐴 ·o 𝐵)) |
| 15 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
| 16 | | onelon 6409 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
| 17 | 16 | ad2ant2rl 749 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ On) |
| 18 | | omcl 8574 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·o 𝑥) ∈ On) |
| 19 | 11, 7, 18 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·o 𝑥) ∈ On) |
| 20 | | oaord 8585 |
. . . . . . . . 9
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·o 𝑥) ∈ On) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·o 𝑥) +o 𝑦) ∈ ((𝐴 ·o 𝑥) +o 𝐴))) |
| 21 | 17, 11, 19, 20 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝑦 ∈ 𝐴 ↔ ((𝐴 ·o 𝑥) +o 𝑦) ∈ ((𝐴 ·o 𝑥) +o 𝐴))) |
| 22 | 15, 21 | mpbid 232 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·o 𝑥) +o 𝑦) ∈ ((𝐴 ·o 𝑥) +o 𝐴)) |
| 23 | | omsuc 8564 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·o suc 𝑥) = ((𝐴 ·o 𝑥) +o 𝐴)) |
| 24 | 11, 7, 23 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → (𝐴 ·o suc 𝑥) = ((𝐴 ·o 𝑥) +o 𝐴)) |
| 25 | 22, 24 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o suc 𝑥)) |
| 26 | 14, 25 | sseldd 3984 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵)) |
| 27 | 26 | ralrimivva 3202 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵)) |
| 28 | | omxpenlem.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·o 𝑥) +o 𝑦)) |
| 29 | 28 | fmpo 8093 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐴 ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ↔ 𝐹:(𝐵 × 𝐴)⟶(𝐴 ·o 𝐵)) |
| 30 | 27, 29 | sylib 218 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)⟶(𝐴 ·o 𝐵)) |
| 31 | 30 | ffnd 6737 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹 Fn (𝐵 × 𝐴)) |
| 32 | | simpll 767 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → 𝐴 ∈ On) |
| 33 | | omcl 8574 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
| 34 | | onelon 6409 |
. . . . . . . 8
⊢ (((𝐴 ·o 𝐵) ∈ On ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → 𝑚 ∈ On) |
| 35 | 33, 34 | sylan 580 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → 𝑚 ∈ On) |
| 36 | | noel 4338 |
. . . . . . . . . . . 12
⊢ ¬
𝑚 ∈
∅ |
| 37 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = ∅ → (𝐴 ·o 𝐵) = (∅
·o 𝐵)) |
| 38 | | om0r 8577 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
·o 𝐵) =
∅) |
| 39 | 37, 38 | sylan9eqr 2799 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ·o 𝐵) = ∅) |
| 40 | 39 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝑚 ∈ (𝐴 ·o 𝐵) ↔ 𝑚 ∈ ∅)) |
| 41 | 36, 40 | mtbiri 327 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → ¬ 𝑚 ∈ (𝐴 ·o 𝐵)) |
| 42 | 41 | ex 412 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → (𝐴 = ∅ → ¬ 𝑚 ∈ (𝐴 ·o 𝐵))) |
| 43 | 42 | necon2ad 2955 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (𝑚 ∈ (𝐴 ·o 𝐵) → 𝐴 ≠ ∅)) |
| 44 | 43 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑚 ∈ (𝐴 ·o 𝐵) → 𝐴 ≠ ∅)) |
| 45 | 44 | imp 406 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → 𝐴 ≠ ∅) |
| 46 | | omeu 8623 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑚 ∈ On ∧ 𝐴 ≠ ∅) →
∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚)) |
| 47 | 32, 35, 45, 46 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → ∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚)) |
| 48 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑚 ∈ V |
| 49 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑛 ∈ V |
| 50 | 48, 49 | brcnv 5893 |
. . . . . . . 8
⊢ (𝑚◡𝐹𝑛 ↔ 𝑛𝐹𝑚) |
| 51 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = ((𝐴 ·o 𝑥) +o 𝑦) → (𝑚 ∈ (𝐴 ·o 𝐵) ↔ ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵))) |
| 52 | 51 | biimpac 478 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (𝐴 ·o 𝐵) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)) → ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵)) |
| 53 | 6 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ On → (𝑥 ∈ 𝐵 → 𝑥 ∈ On)) |
| 54 | 53 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝐵 → 𝑥 ∈ On)) |
| 55 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
| 56 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑥 ∈ On) |
| 57 | 55, 56, 18 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·o 𝑥) ∈ On) |
| 58 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑦 ∈ 𝐴) |
| 59 | 55, 58, 16 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑦 ∈ On) |
| 60 | | oaword1 8590 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ·o 𝑥) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o 𝑥) ⊆ ((𝐴 ·o 𝑥) +o 𝑦)) |
| 61 | 57, 59, 60 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·o 𝑥) ⊆ ((𝐴 ·o 𝑥) +o 𝑦)) |
| 62 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵)) |
| 63 | 33 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
| 64 | | ontr2 6431 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ·o 𝑥) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On) → (((𝐴 ·o 𝑥) ⊆ ((𝐴 ·o 𝑥) +o 𝑦) ∧ ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵)) → (𝐴 ·o 𝑥) ∈ (𝐴 ·o 𝐵))) |
| 65 | 57, 63, 64 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (((𝐴 ·o 𝑥) ⊆ ((𝐴 ·o 𝑥) +o 𝑦) ∧ ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵)) → (𝐴 ·o 𝑥) ∈ (𝐴 ·o 𝐵))) |
| 66 | 61, 62, 65 | mp2and 699 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·o 𝑥) ∈ (𝐴 ·o 𝐵)) |
| 67 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝐵 ∈ On) |
| 68 | 62 | ne0d 4342 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·o 𝐵) ≠ ∅) |
| 69 | | on0eln0 6440 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ·o 𝐵) ∈ On → (∅
∈ (𝐴
·o 𝐵)
↔ (𝐴
·o 𝐵)
≠ ∅)) |
| 70 | 63, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·o 𝐵) ↔ (𝐴 ·o 𝐵) ≠ ∅)) |
| 71 | 68, 70 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ∅ ∈ (𝐴 ·o 𝐵)) |
| 72 | | om00el 8614 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ (𝐴
·o 𝐵)
↔ (∅ ∈ 𝐴
∧ ∅ ∈ 𝐵))) |
| 73 | 72 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·o 𝐵) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵))) |
| 74 | 71, 73 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵)) |
| 75 | 74 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → ∅ ∈ 𝐴) |
| 76 | | omord2 8605 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑥 ∈ 𝐵 ↔ (𝐴 ·o 𝑥) ∈ (𝐴 ·o 𝐵))) |
| 77 | 56, 67, 55, 75, 76 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → (𝑥 ∈ 𝐵 ↔ (𝐴 ·o 𝑥) ∈ (𝐴 ·o 𝐵))) |
| 78 | 66, 77 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 ∈ On) → 𝑥 ∈ 𝐵) |
| 79 | 78 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ On → 𝑥 ∈ 𝐵)) |
| 80 | 54, 79 | impbid 212 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵) ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ On)) |
| 81 | 80 | expr 456 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵)) → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ On))) |
| 82 | 81 | pm5.32rd 578 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ((𝐴 ·o 𝑥) +o 𝑦) ∈ (𝐴 ·o 𝐵)) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴))) |
| 83 | 52, 82 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑚 ∈ (𝐴 ·o 𝐵) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦))) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴))) |
| 84 | 83 | expr 456 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → (𝑚 = ((𝐴 ·o 𝑥) +o 𝑦) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ 𝐴)))) |
| 85 | 84 | pm5.32rd 578 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))) |
| 86 | | eqcom 2744 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((𝐴 ·o 𝑥) +o 𝑦) ↔ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚) |
| 87 | 86 | anbi2i 623 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚)) |
| 88 | 85, 87 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚))) |
| 89 | 88 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦))) ↔ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚)))) |
| 90 | | an12 645 |
. . . . . . . . . . 11
⊢ ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚))) |
| 91 | 89, 90 | bitrdi 287 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → ((𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦))) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚)))) |
| 92 | 91 | 2exbidv 1924 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → (∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦))) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚)))) |
| 93 | | df-mpo 7436 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·o 𝑥) +o 𝑦)) = {〈〈𝑥, 𝑦〉, 𝑚〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦))} |
| 94 | | dfoprab2 7491 |
. . . . . . . . . . . 12
⊢
{〈〈𝑥,
𝑦〉, 𝑚〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦))} = {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))} |
| 95 | 28, 93, 94 | 3eqtri 2769 |
. . . . . . . . . . 11
⊢ 𝐹 = {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))} |
| 96 | 95 | breqi 5149 |
. . . . . . . . . 10
⊢ (𝑛𝐹𝑚 ↔ 𝑛{〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))}𝑚) |
| 97 | | df-br 5144 |
. . . . . . . . . 10
⊢ (𝑛{〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))}𝑚 ↔ 〈𝑛, 𝑚〉 ∈ {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))}) |
| 98 | | opabidw 5529 |
. . . . . . . . . 10
⊢
(〈𝑛, 𝑚〉 ∈ {〈𝑛, 𝑚〉 ∣ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))} ↔ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))) |
| 99 | 96, 97, 98 | 3bitri 297 |
. . . . . . . . 9
⊢ (𝑛𝐹𝑚 ↔ ∃𝑥∃𝑦(𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑚 = ((𝐴 ·o 𝑥) +o 𝑦)))) |
| 100 | | r2ex 3196 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚))) |
| 101 | 92, 99, 100 | 3bitr4g 314 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → (𝑛𝐹𝑚 ↔ ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚))) |
| 102 | 50, 101 | bitrid 283 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → (𝑚◡𝐹𝑛 ↔ ∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚))) |
| 103 | 102 | eubidv 2586 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → (∃!𝑛 𝑚◡𝐹𝑛 ↔ ∃!𝑛∃𝑥 ∈ On ∃𝑦 ∈ 𝐴 (𝑛 = 〈𝑥, 𝑦〉 ∧ ((𝐴 ·o 𝑥) +o 𝑦) = 𝑚))) |
| 104 | 47, 103 | mpbird 257 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·o 𝐵)) → ∃!𝑛 𝑚◡𝐹𝑛) |
| 105 | 104 | ralrimiva 3146 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑚 ∈ (𝐴 ·o 𝐵)∃!𝑛 𝑚◡𝐹𝑛) |
| 106 | | fnres 6695 |
. . . 4
⊢ ((◡𝐹 ↾ (𝐴 ·o 𝐵)) Fn (𝐴 ·o 𝐵) ↔ ∀𝑚 ∈ (𝐴 ·o 𝐵)∃!𝑛 𝑚◡𝐹𝑛) |
| 107 | 105, 106 | sylibr 234 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (◡𝐹 ↾ (𝐴 ·o 𝐵)) Fn (𝐴 ·o 𝐵)) |
| 108 | | relcnv 6122 |
. . . . 5
⊢ Rel ◡𝐹 |
| 109 | | df-rn 5696 |
. . . . . 6
⊢ ran 𝐹 = dom ◡𝐹 |
| 110 | 30 | frnd 6744 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ran 𝐹 ⊆ (𝐴 ·o 𝐵)) |
| 111 | 109, 110 | eqsstrrid 4023 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → dom ◡𝐹 ⊆ (𝐴 ·o 𝐵)) |
| 112 | | relssres 6040 |
. . . . 5
⊢ ((Rel
◡𝐹 ∧ dom ◡𝐹 ⊆ (𝐴 ·o 𝐵)) → (◡𝐹 ↾ (𝐴 ·o 𝐵)) = ◡𝐹) |
| 113 | 108, 111,
112 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (◡𝐹 ↾ (𝐴 ·o 𝐵)) = ◡𝐹) |
| 114 | 113 | fneq1d 6661 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((◡𝐹 ↾ (𝐴 ·o 𝐵)) Fn (𝐴 ·o 𝐵) ↔ ◡𝐹 Fn (𝐴 ·o 𝐵))) |
| 115 | 107, 114 | mpbid 232 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ◡𝐹 Fn (𝐴 ·o 𝐵)) |
| 116 | | dff1o4 6856 |
. 2
⊢ (𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·o 𝐵) ↔ (𝐹 Fn (𝐵 × 𝐴) ∧ ◡𝐹 Fn (𝐴 ·o 𝐵))) |
| 117 | 31, 115, 116 | sylanbrc 583 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·o 𝐵)) |