Theorem fin1a2lem4 9430

Description: Lemma for fin1a2 9442. (Contributed by Stefan O'Rear, 7-Nov-2014.)

Hypothesis

Ref	Expression
fin1a2lem.b	⊢ 𝐸 = (𝑥 ∈ ω ↦ (2𝑜 ·𝑜 𝑥))

Assertion

Ref	Expression
fin1a2lem4	⊢ 𝐸:ω–1-1→ω

Proof of Theorem fin1a2lem4

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fin1a2lem.b	. . 3 ⊢ 𝐸 = (𝑥 ∈ ω ↦ (2𝑜 ·𝑜 𝑥))
2		2onn 7877	. . . 4 ⊢ 2𝑜 ∈ ω
3		nnmcl 7849	. . . 4 ⊢ ((2𝑜 ∈ ω ∧ 𝑥 ∈ ω) → (2𝑜 ·𝑜 𝑥) ∈ ω)
4	2, 3	mpan 670	. . 3 ⊢ (𝑥 ∈ ω → (2𝑜 ·𝑜 𝑥) ∈ ω)
5	1, 4	fmpti 6527	. 2 ⊢ 𝐸:ω⟶ω
6	1	fin1a2lem3 9429	. . . . . 6 ⊢ (𝑎 ∈ ω → (𝐸‘𝑎) = (2𝑜 ·𝑜 𝑎))
7	1	fin1a2lem3 9429	. . . . . 6 ⊢ (𝑏 ∈ ω → (𝐸‘𝑏) = (2𝑜 ·𝑜 𝑏))
8	6, 7	eqeqan12d 2787	. . . . 5 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝐸‘𝑎) = (𝐸‘𝑏) ↔ (2𝑜 ·𝑜 𝑎) = (2𝑜 ·𝑜 𝑏)))
9		2on 7725	. . . . . . 7 ⊢ 2𝑜 ∈ On
10	9	a1i 11	. . . . . 6 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → 2𝑜 ∈ On)
11		nnon 7221	. . . . . . 7 ⊢ (𝑎 ∈ ω → 𝑎 ∈ On)
12	11	adantr 466	. . . . . 6 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → 𝑎 ∈ On)
13		nnon 7221	. . . . . . 7 ⊢ (𝑏 ∈ ω → 𝑏 ∈ On)
14	13	adantl 467	. . . . . 6 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → 𝑏 ∈ On)
15		0lt1o 7741	. . . . . . . . 9 ⊢ ∅ ∈ 1𝑜
16		elelsuc 5939	. . . . . . . . 9 ⊢ (∅ ∈ 1𝑜 → ∅ ∈ suc 1𝑜)
17	15, 16	ax-mp 5	. . . . . . . 8 ⊢ ∅ ∈ suc 1𝑜
18		df-2o 7717	. . . . . . . 8 ⊢ 2𝑜 = suc 1𝑜
19	17, 18	eleqtrri 2849	. . . . . . 7 ⊢ ∅ ∈ 2𝑜
20	19	a1i 11	. . . . . 6 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ∅ ∈ 2𝑜)
21		omcan 7806	. . . . . 6 ⊢ (((2𝑜 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∅ ∈ 2𝑜) → ((2𝑜 ·𝑜 𝑎) = (2𝑜 ·𝑜 𝑏) ↔ 𝑎 = 𝑏))
22	10, 12, 14, 20, 21	syl31anc 1479	. . . . 5 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((2𝑜 ·𝑜 𝑎) = (2𝑜 ·𝑜 𝑏) ↔ 𝑎 = 𝑏))
23	8, 22	bitrd 268	. . . 4 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝐸‘𝑎) = (𝐸‘𝑏) ↔ 𝑎 = 𝑏))
24	23	biimpd 219	. . 3 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝐸‘𝑎) = (𝐸‘𝑏) → 𝑎 = 𝑏))
25	24	rgen2a 3126	. 2 ⊢ ∀𝑎 ∈ ω ∀𝑏 ∈ ω ((𝐸‘𝑎) = (𝐸‘𝑏) → 𝑎 = 𝑏)
26		dff13 6657	. 2 ⊢ (𝐸:ω–1-1→ω ↔ (𝐸:ω⟶ω ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω ((𝐸‘𝑎) = (𝐸‘𝑏) → 𝑎 = 𝑏)))
27	5, 25, 26	mpbir2an 690	1 ⊢ 𝐸:ω–1-1→ω

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ∀wral 3061  ∅c0 4063   ↦ cmpt 4864  Oncon0 5865  suc csuc 5867  ⟶wf 6026  –1-1→wf1 6027  ‘cfv 6030  (class class class)co 6795  ωcom 7215  1_𝑜c1o 7709  2_𝑜c2o 7710   ·_𝑜 comu 7714

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 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099

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-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 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-om 7216  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-1o 7716  df-2o 7717  df-oadd 7720  df-omul 7721

This theorem is referenced by:  fin1a2lem5  9431  fin1a2lem6  9432  fin1a2lem7  9433