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		onsuc	⊢ ( 𝑥 ∈ 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 𝐵 ) )