Metamath Proof Explorer

Theorem omxpenlem

Description: Lemma for omxpen . (Contributed by Mario Carneiro, 3-Mar-2013) (Revised by Mario Carneiro, 25-May-2015)

Ref Expression
Hypothesis omxpenlem.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) )
Assertion omxpenlem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 ·o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 omxpenlem.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) )
2 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
3 2 ad2antlr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → Ord 𝐵 )
4 simprl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐵 )
5 ordsucss ⊢ ( Ord 𝐵 → ( 𝑥 ∈ 𝐵 → suc 𝑥 ⊆ 𝐵 ) )
6 3 4 5 sylc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → suc 𝑥 ⊆ 𝐵 )
7 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
8 7 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ On )
9 suceloni ⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
10 8 9 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → suc 𝑥 ∈ On )
11 simplr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐵 ∈ On )
12 simpll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐴 ∈ On )
13 omwordi ⊢ ( ( suc 𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( suc 𝑥 ⊆ 𝐵 → ( 𝐴 ·o suc 𝑥 ) ⊆ ( 𝐴 ·o 𝐵 ) ) )
14 10 11 12 13 syl3anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( suc 𝑥 ⊆ 𝐵 → ( 𝐴 ·o suc 𝑥 ) ⊆ ( 𝐴 ·o 𝐵 ) ) )
15 6 14 mpd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐴 ·o suc 𝑥 ) ⊆ ( 𝐴 ·o 𝐵 ) )
16 simprr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
17 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
18 17 ad2ant2rl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ On )
19 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ·o 𝑥 ) ∈ On )
20 12 8 19 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐴 ·o 𝑥 ) ∈ On )
21 oaord ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ∧ ( 𝐴 ·o 𝑥 ) ∈ On ) → ( 𝑦 ∈ 𝐴 ↔ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) ) )
22 18 12 20 21 syl3anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 ∈ 𝐴 ↔ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) ) )
23 16 22 mpbid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) )
24 omsuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ·o suc 𝑥 ) = ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) )
25 12 8 24 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐴 ·o suc 𝑥 ) = ( ( 𝐴 ·o 𝑥 ) +o 𝐴 ) )
26 23 25 eleqtrrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o suc 𝑥 ) )
27 15 26 sseldd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) )
28 27 ralrimivva ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) )
29 1 fmpo ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐴 ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ↔ 𝐹 : ( 𝐵 × 𝐴 ) ⟶ ( 𝐴 ·o 𝐵 ) )
30 28 29 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : ( 𝐵 × 𝐴 ) ⟶ ( 𝐴 ·o 𝐵 ) )
31 30 ffnd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 Fn ( 𝐵 × 𝐴 ) )
32 simpll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → 𝐴 ∈ On )
33 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
34 onelon ⊢ ( ( ( 𝐴 ·o 𝐵 ) ∈ On ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → 𝑚 ∈ On )
35 33 34 sylan ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → 𝑚 ∈ On )
36 noel ⊢ ¬ 𝑚 ∈ ∅
37 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ·o 𝐵 ) = ( ∅ ·o 𝐵 ) )
38 om0r ⊢ ( 𝐵 ∈ On → ( ∅ ·o 𝐵 ) = ∅ )
39 37 38 sylan9eqr ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( 𝐴 ·o 𝐵 ) = ∅ )
40 39 eleq2d ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ↔ 𝑚 ∈ ∅ ) )
41 36 40 mtbiri ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ¬ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) )
42 41 ex ⊢ ( 𝐵 ∈ On → ( 𝐴 = ∅ → ¬ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) )
43 42 necon2ad ⊢ ( 𝐵 ∈ On → ( 𝑚 ∈ ( 𝐴 ·o 𝐵 ) → 𝐴 ≠ ∅ ) )
44 43 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑚 ∈ ( 𝐴 ·o 𝐵 ) → 𝐴 ≠ ∅ ) )
45 44 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → 𝐴 ≠ ∅ )
46 omeu ⊢ ( ( 𝐴 ∈ On ∧ 𝑚 ∈ On ∧ 𝐴 ≠ ∅ ) → ∃! 𝑛 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) )
47 32 35 45 46 syl3anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ∃! 𝑛 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) )
48 vex ⊢ 𝑚 ∈ V
49 vex ⊢ 𝑛 ∈ V
50 48 49 brcnv ⊢ ( 𝑚 ◡ 𝐹 𝑛 ↔ 𝑛 𝐹 𝑚 )
51 eleq1 ⊢ ( 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) → ( 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ↔ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
52 51 biimpac ⊢ ( ( 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) )
53 7 ex ⊢ ( 𝐵 ∈ On → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ On ) )
54 53 ad2antlr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ On ) )
55 simplll ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → 𝐴 ∈ On )
56 simpr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → 𝑥 ∈ On )
57 55 56 19 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( 𝐴 ·o 𝑥 ) ∈ On )
58 simplrr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → 𝑦 ∈ 𝐴 )
59 55 58 17 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → 𝑦 ∈ On )
60 oaword1 ⊢ ( ( ( 𝐴 ·o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o 𝑥 ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) )
61 57 59 60 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( 𝐴 ·o 𝑥 ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) )
62 simplrl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) )
63 33 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
64 ontr2 ⊢ ( ( ( 𝐴 ·o 𝑥 ) ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ) → ( ( ( 𝐴 ·o 𝑥 ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ) → ( 𝐴 ·o 𝑥 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
65 57 63 64 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( ( ( 𝐴 ·o 𝑥 ) ⊆ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ) → ( 𝐴 ·o 𝑥 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
66 61 62 65 mp2and ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( 𝐴 ·o 𝑥 ) ∈ ( 𝐴 ·o 𝐵 ) )
67 simpllr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → 𝐵 ∈ On )
68 62 ne0d ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( 𝐴 ·o 𝐵 ) ≠ ∅ )
69 on0eln0 ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → ( ∅ ∈ ( 𝐴 ·o 𝐵 ) ↔ ( 𝐴 ·o 𝐵 ) ≠ ∅ ) )
70 63 69 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( ∅ ∈ ( 𝐴 ·o 𝐵 ) ↔ ( 𝐴 ·o 𝐵 ) ≠ ∅ ) )
71 68 70 mpbird ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ∅ ∈ ( 𝐴 ·o 𝐵 ) )
72 om00el ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ ( 𝐴 ·o 𝐵 ) ↔ ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵 ) ) )
73 72 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( ∅ ∈ ( 𝐴 ·o 𝐵 ) ↔ ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵 ) ) )
74 71 73 mpbid ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵 ) )
75 74 simpld ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ∅ ∈ 𝐴 )
76 omord2 ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝐴 ·o 𝑥 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
77 56 67 55 75 76 syl31anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝐴 ·o 𝑥 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
78 66 77 mpbird ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ∈ On ) → 𝑥 ∈ 𝐵 )
79 78 ex ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∈ On → 𝑥 ∈ 𝐵 ) )
80 54 79 impbid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ On ) )
81 80 expr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ) → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ On ) ) )
82 81 pm5.32rd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ∈ ( 𝐴 ·o 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ) )
83 52 82 sylan2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ) )
84 83 expr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ) ) )
85 84 pm5.32rd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) )
86 eqcom ⊢ ( 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ↔ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 )
87 86 anbi2i ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) )
88 85 87 bitrdi ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) )
89 88 anbi2d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) ↔ ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) ) )
90 an12 ⊢ ( ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) )
91 89 90 bitrdi ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) ) )
92 91 2exbidv ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) ) )
93 df-mpo ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) }
94 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) } = { ⟨ 𝑛 , 𝑚 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) }
95 1 93 94 3eqtri ⊢ 𝐹 = { ⟨ 𝑛 , 𝑚 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) }
96 95 breqi ⊢ ( 𝑛 𝐹 𝑚 ↔ 𝑛 { ⟨ 𝑛 , 𝑚 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) } 𝑚 )
97 df-br ⊢ ( 𝑛 { ⟨ 𝑛 , 𝑚 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) } 𝑚 ↔ ⟨ 𝑛 , 𝑚 ⟩ ∈ { ⟨ 𝑛 , 𝑚 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) } )
98 opabidw ⊢ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ { ⟨ 𝑛 , 𝑚 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) )
99 96 97 98 3bitri ⊢ ( 𝑛 𝐹 𝑚 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑚 = ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) ) )
100 r2ex ⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) )
101 92 99 100 3bitr4g ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( 𝑛 𝐹 𝑚 ↔ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) )
102 50 101 bitrid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( 𝑚 ◡ 𝐹 𝑛 ↔ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) )
103 102 eubidv ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ( ∃! 𝑛 𝑚 ◡ 𝐹 𝑛 ↔ ∃! 𝑛 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑛 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝑚 ) ) )
104 47 103 mpbird ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ) → ∃! 𝑛 𝑚 ◡ 𝐹 𝑛 )
105 104 ralrimiva ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∀ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ∃! 𝑛 𝑚 ◡ 𝐹 𝑛 )
106 fnres ⊢ ( ( ◡ 𝐹 ↾ ( 𝐴 ·o 𝐵 ) ) Fn ( 𝐴 ·o 𝐵 ) ↔ ∀ 𝑚 ∈ ( 𝐴 ·o 𝐵 ) ∃! 𝑛 𝑚 ◡ 𝐹 𝑛 )
107 105 106 sylibr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ◡ 𝐹 ↾ ( 𝐴 ·o 𝐵 ) ) Fn ( 𝐴 ·o 𝐵 ) )
108 relcnv ⊢ Rel ◡ 𝐹
109 df-rn ⊢ ran 𝐹 = dom ◡ 𝐹
110 30 frnd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ran 𝐹 ⊆ ( 𝐴 ·o 𝐵 ) )
111 109 110 eqsstrrid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → dom ◡ 𝐹 ⊆ ( 𝐴 ·o 𝐵 ) )
112 relssres ⊢ ( ( Rel ◡ 𝐹 ∧ dom ◡ 𝐹 ⊆ ( 𝐴 ·o 𝐵 ) ) → ( ◡ 𝐹 ↾ ( 𝐴 ·o 𝐵 ) ) = ◡ 𝐹 )
113 108 111 112 sylancr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ◡ 𝐹 ↾ ( 𝐴 ·o 𝐵 ) ) = ◡ 𝐹 )
114 113 fneq1d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ◡ 𝐹 ↾ ( 𝐴 ·o 𝐵 ) ) Fn ( 𝐴 ·o 𝐵 ) ↔ ◡ 𝐹 Fn ( 𝐴 ·o 𝐵 ) ) )
115 107 114 mpbid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ◡ 𝐹 Fn ( 𝐴 ·o 𝐵 ) )
116 dff1o4 ⊢ ( 𝐹 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 ·o 𝐵 ) ↔ ( 𝐹 Fn ( 𝐵 × 𝐴 ) ∧ ◡ 𝐹 Fn ( 𝐴 ·o 𝐵 ) ) )
117 31 115 116 sylanbrc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 ·o 𝐵 ) )