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 syl5bb ( ( ( 𝐴 ∈ 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 𝐵 ) )