MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omxpenlem Structured version   Visualization version   GIF version

Theorem omxpenlem 8217
Description: Lemma for omxpen 8218. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.)
Hypothesis
Ref Expression
omxpenlem.1 𝐹 = (𝑥𝐵, 𝑦𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))
Assertion
Ref Expression
omxpenlem ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·𝑜 𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem omxpenlem
Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eloni 5876 . . . . . . . . 9 (𝐵 ∈ On → Ord 𝐵)
21ad2antlr 706 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → Ord 𝐵)
3 simprl 754 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → 𝑥𝐵)
4 ordsucss 7165 . . . . . . . 8 (Ord 𝐵 → (𝑥𝐵 → suc 𝑥𝐵))
52, 3, 4sylc 65 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → suc 𝑥𝐵)
6 onelon 5891 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑥𝐵) → 𝑥 ∈ On)
76ad2ant2lr 742 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → 𝑥 ∈ On)
8 suceloni 7160 . . . . . . . . 9 (𝑥 ∈ On → suc 𝑥 ∈ On)
97, 8syl 17 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → suc 𝑥 ∈ On)
10 simplr 752 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → 𝐵 ∈ On)
11 simpll 750 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → 𝐴 ∈ On)
12 omwordi 7805 . . . . . . . 8 ((suc 𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) → (suc 𝑥𝐵 → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵)))
139, 10, 11, 12syl3anc 1476 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → (suc 𝑥𝐵 → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵)))
145, 13mpd 15 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → (𝐴 ·𝑜 suc 𝑥) ⊆ (𝐴 ·𝑜 𝐵))
15 simprr 756 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → 𝑦𝐴)
16 onelon 5891 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑦𝐴) → 𝑦 ∈ On)
1716ad2ant2rl 743 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → 𝑦 ∈ On)
18 omcl 7770 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ On)
1911, 7, 18syl2anc 573 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → (𝐴 ·𝑜 𝑥) ∈ On)
20 oaord 7781 . . . . . . . . 9 ((𝑦 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜 𝑥) ∈ On) → (𝑦𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)))
2117, 11, 19, 20syl3anc 1476 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → (𝑦𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)))
2215, 21mpbid 222 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
23 omsuc 7760 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
2411, 7, 23syl2anc 573 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → (𝐴 ·𝑜 suc 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))
2522, 24eleqtrrd 2853 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 suc 𝑥))
2614, 25sseldd 3753 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥𝐵𝑦𝐴)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵))
2726ralrimivva 3120 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑥𝐵𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵))
28 omxpenlem.1 . . . . 5 𝐹 = (𝑥𝐵, 𝑦𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))
2928fmpt2 7387 . . . 4 (∀𝑥𝐵𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ↔ 𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵))
3027, 29sylib 208 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵))
31 ffn 6185 . . 3 (𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵) → 𝐹 Fn (𝐵 × 𝐴))
3230, 31syl 17 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹 Fn (𝐵 × 𝐴))
33 simpll 750 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝐴 ∈ On)
34 omcl 7770 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 𝐵) ∈ On)
35 onelon 5891 . . . . . . . 8 (((𝐴 ·𝑜 𝐵) ∈ On ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝑚 ∈ On)
3634, 35sylan 569 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝑚 ∈ On)
37 noel 4067 . . . . . . . . . . . 12 ¬ 𝑚 ∈ ∅
38 oveq1 6800 . . . . . . . . . . . . . 14 (𝐴 = ∅ → (𝐴 ·𝑜 𝐵) = (∅ ·𝑜 𝐵))
39 om0r 7773 . . . . . . . . . . . . . 14 (𝐵 ∈ On → (∅ ·𝑜 𝐵) = ∅)
4038, 39sylan9eqr 2827 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ·𝑜 𝐵) = ∅)
4140eleq2d 2836 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) ↔ 𝑚 ∈ ∅))
4237, 41mtbiri 316 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ 𝐴 = ∅) → ¬ 𝑚 ∈ (𝐴 ·𝑜 𝐵))
4342ex 397 . . . . . . . . . 10 (𝐵 ∈ On → (𝐴 = ∅ → ¬ 𝑚 ∈ (𝐴 ·𝑜 𝐵)))
4443necon2ad 2958 . . . . . . . . 9 (𝐵 ∈ On → (𝑚 ∈ (𝐴 ·𝑜 𝐵) → 𝐴 ≠ ∅))
4544adantl 467 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) → 𝐴 ≠ ∅))
4645imp 393 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → 𝐴 ≠ ∅)
47 omeu 7819 . . . . . . 7 ((𝐴 ∈ On ∧ 𝑚 ∈ On ∧ 𝐴 ≠ ∅) → ∃!𝑛𝑥 ∈ On ∃𝑦𝐴 (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))
4833, 36, 46, 47syl3anc 1476 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ∃!𝑛𝑥 ∈ On ∃𝑦𝐴 (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))
49 vex 3354 . . . . . . . . 9 𝑚 ∈ V
50 vex 3354 . . . . . . . . 9 𝑛 ∈ V
5149, 50brcnv 5443 . . . . . . . 8 (𝑚𝐹𝑛𝑛𝐹𝑚)
52 eleq1 2838 . . . . . . . . . . . . . . . . 17 (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) → (𝑚 ∈ (𝐴 ·𝑜 𝐵) ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)))
5352biimpac 464 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵))
546ex 397 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ On → (𝑥𝐵𝑥 ∈ On))
5554ad2antlr 706 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) → (𝑥𝐵𝑥 ∈ On))
56 simplll 758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → 𝐴 ∈ On)
57 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
5856, 57, 18syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ On)
59 simplrr 763 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → 𝑦𝐴)
6056, 59, 16syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → 𝑦 ∈ On)
61 oaword1 7786 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ·𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))
6258, 60, 61syl2anc 573 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))
63 simplrl 762 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵))
6434ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝐵) ∈ On)
65 ontr2 5915 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ·𝑜 𝑥) ∈ On ∧ (𝐴 ·𝑜 𝐵) ∈ On) → (((𝐴 ·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵)))
6658, 64, 65syl2anc 573 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (((𝐴 ·𝑜 𝑥) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵)))
6762, 63, 66mp2and 679 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵))
68 simpllr 760 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → 𝐵 ∈ On)
69 ne0i 4069 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) → (𝐴 ·𝑜 𝐵) ≠ ∅)
7063, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (𝐴 ·𝑜 𝐵) ≠ ∅)
71 on0eln0 5923 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ·𝑜 𝐵) ∈ On → (∅ ∈ (𝐴 ·𝑜 𝐵) ↔ (𝐴 ·𝑜 𝐵) ≠ ∅))
7264, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·𝑜 𝐵) ↔ (𝐴 ·𝑜 𝐵) ≠ ∅))
7370, 72mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → ∅ ∈ (𝐴 ·𝑜 𝐵))
74 om00el 7810 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅ ∈ (𝐴 ·𝑜 𝐵) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵)))
7574ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ (𝐴 ·𝑜 𝐵) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵)))
7673, 75mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵))
7776simpld 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → ∅ ∈ 𝐴)
78 omord2 7801 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑥𝐵 ↔ (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵)))
7957, 68, 56, 77, 78syl31anc 1479 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → (𝑥𝐵 ↔ (𝐴 ·𝑜 𝑥) ∈ (𝐴 ·𝑜 𝐵)))
8067, 79mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) ∧ 𝑥 ∈ On) → 𝑥𝐵)
8180ex 397 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) → (𝑥 ∈ On → 𝑥𝐵))
8255, 81impbid 202 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑦𝐴)) → (𝑥𝐵𝑥 ∈ On))
8382expr 444 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) → (𝑦𝐴 → (𝑥𝐵𝑥 ∈ On)))
8483pm5.32rd 567 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ∈ (𝐴 ·𝑜 𝐵)) → ((𝑥𝐵𝑦𝐴) ↔ (𝑥 ∈ On ∧ 𝑦𝐴)))
8553, 84sylan2 580 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑚 ∈ (𝐴 ·𝑜 𝐵) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) → ((𝑥𝐵𝑦𝐴) ↔ (𝑥 ∈ On ∧ 𝑦𝐴)))
8685expr 444 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) → ((𝑥𝐵𝑦𝐴) ↔ (𝑥 ∈ On ∧ 𝑦𝐴))))
8786pm5.32rd 567 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))))
88 eqcom 2778 . . . . . . . . . . . . . 14 (𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)
8988anbi2i 609 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ 𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))
9087, 89syl6bb 276 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))
9190anbi2d 614 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ((𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))))
92 an12 624 . . . . . . . . . . 11 ((𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)) ↔ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))
9391, 92syl6bb 276 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ((𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))))
94932exbidv 2004 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))) ↔ ∃𝑥𝑦((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚))))
95 df-mpt2 6798 . . . . . . . . . . . 12 (𝑥𝐵, 𝑦𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) = {⟨⟨𝑥, 𝑦⟩, 𝑚⟩ ∣ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))}
96 dfoprab2 6848 . . . . . . . . . . . 12 {⟨⟨𝑥, 𝑦⟩, 𝑚⟩ ∣ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))} = {⟨𝑛, 𝑚⟩ ∣ ∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}
9728, 95, 963eqtri 2797 . . . . . . . . . . 11 𝐹 = {⟨𝑛, 𝑚⟩ ∣ ∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}
9897breqi 4792 . . . . . . . . . 10 (𝑛𝐹𝑚𝑛{⟨𝑛, 𝑚⟩ ∣ ∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}𝑚)
99 df-br 4787 . . . . . . . . . 10 (𝑛{⟨𝑛, 𝑚⟩ ∣ ∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))}𝑚 ↔ ⟨𝑛, 𝑚⟩ ∈ {⟨𝑛, 𝑚⟩ ∣ ∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))})
100 opabid 5115 . . . . . . . . . 10 (⟨𝑛, 𝑚⟩ ∈ {⟨𝑛, 𝑚⟩ ∣ ∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)))} ↔ ∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))))
10198, 99, 1003bitri 286 . . . . . . . . 9 (𝑛𝐹𝑚 ↔ ∃𝑥𝑦(𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥𝐵𝑦𝐴) ∧ 𝑚 = ((𝐴 ·𝑜 𝑥) +𝑜 𝑦))))
102 r2ex 3209 . . . . . . . . 9 (∃𝑥 ∈ On ∃𝑦𝐴 (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚) ↔ ∃𝑥𝑦((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))
10394, 101, 1023bitr4g 303 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑛𝐹𝑚 ↔ ∃𝑥 ∈ On ∃𝑦𝐴 (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))
10451, 103syl5bb 272 . . . . . . 7 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (𝑚𝐹𝑛 ↔ ∃𝑥 ∈ On ∃𝑦𝐴 (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))
105104eubidv 2638 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → (∃!𝑛 𝑚𝐹𝑛 ↔ ∃!𝑛𝑥 ∈ On ∃𝑦𝐴 (𝑛 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝑚)))
10648, 105mpbird 247 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑚 ∈ (𝐴 ·𝑜 𝐵)) → ∃!𝑛 𝑚𝐹𝑛)
107106ralrimiva 3115 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∀𝑚 ∈ (𝐴 ·𝑜 𝐵)∃!𝑛 𝑚𝐹𝑛)
108 fnres 6147 . . . 4 ((𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵) ↔ ∀𝑚 ∈ (𝐴 ·𝑜 𝐵)∃!𝑛 𝑚𝐹𝑛)
109107, 108sylibr 224 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵))
110 relcnv 5644 . . . . 5 Rel 𝐹
111 df-rn 5260 . . . . . 6 ran 𝐹 = dom 𝐹
112 frn 6193 . . . . . . 7 (𝐹:(𝐵 × 𝐴)⟶(𝐴 ·𝑜 𝐵) → ran 𝐹 ⊆ (𝐴 ·𝑜 𝐵))
11330, 112syl 17 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ran 𝐹 ⊆ (𝐴 ·𝑜 𝐵))
114111, 113syl5eqssr 3799 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → dom 𝐹 ⊆ (𝐴 ·𝑜 𝐵))
115 relssres 5578 . . . . 5 ((Rel 𝐹 ∧ dom 𝐹 ⊆ (𝐴 ·𝑜 𝐵)) → (𝐹 ↾ (𝐴 ·𝑜 𝐵)) = 𝐹)
116110, 114, 115sylancr 575 . . . 4 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹 ↾ (𝐴 ·𝑜 𝐵)) = 𝐹)
117116fneq1d 6121 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐹 ↾ (𝐴 ·𝑜 𝐵)) Fn (𝐴 ·𝑜 𝐵) ↔ 𝐹 Fn (𝐴 ·𝑜 𝐵)))
118109, 117mpbid 222 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹 Fn (𝐴 ·𝑜 𝐵))
119 dff1o4 6286 . 2 (𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·𝑜 𝐵) ↔ (𝐹 Fn (𝐵 × 𝐴) ∧ 𝐹 Fn (𝐴 ·𝑜 𝐵)))
12032, 118, 119sylanbrc 572 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·𝑜 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145  ∃!weu 2618  wne 2943  wral 3061  wrex 3062  wss 3723  c0 4063  cop 4322   class class class wbr 4786  {copab 4846   × cxp 5247  ccnv 5248  dom cdm 5249  ran crn 5250  cres 5251  Rel wrel 5254  Ord word 5865  Oncon0 5866  suc csuc 5868   Fn wfn 6026  wf 6027  1-1-ontowf1o 6030  (class class class)co 6793  {coprab 6794  cmpt2 6795   +𝑜 coa 7710   ·𝑜 comu 7711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-omul 7718
This theorem is referenced by:  omxpen  8218  omf1o  8219  infxpenc  9041
  Copyright terms: Public domain W3C validator