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 ⊢ F = x ∈ B , y ∈ A ⟼ A ⋅ 𝑜 x + 𝑜 y
Assertion omxpenlem ⊢ A ∈ On ∧ B ∈ On → F : B × A ⟶ 1-1 onto A ⋅ 𝑜 B

Proof

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