coe1mul2lem1

Description: An equivalence for coe1mul2 . (Contributed by Stefan O'Rear, 25-Mar-2015)

		Ref	Expression
	Assertion	coe1mul2lem1	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( 𝑋 ∘_r ≤ ( 1_o × { 𝐴 } ) ↔ ( 𝑋 ‘ ∅ ) ∈ ( 0 ... 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1on	⊢ 1_o ∈ On
2	1	a1i	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → 1_o ∈ On )
3		fvexd	⊢ ( ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑎 ∈ 1_o ) → ( 𝑋 ‘ ∅ ) ∈ V )
4		simpll	⊢ ( ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑎 ∈ 1_o ) → 𝐴 ∈ ℕ₀ )
5		df1o2	⊢ 1_o = { ∅ }
6		nn0ex	⊢ ℕ₀ ∈ V
7		0ex	⊢ ∅ ∈ V
8	5 6 7	mapsnconst	⊢ ( 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) → 𝑋 = ( 1_o × { ( 𝑋 ‘ ∅ ) } ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → 𝑋 = ( 1_o × { ( 𝑋 ‘ ∅ ) } ) )
10		fconstmpt	⊢ ( 1_o × { ( 𝑋 ‘ ∅ ) } ) = ( 𝑎 ∈ 1_o ↦ ( 𝑋 ‘ ∅ ) )
11	9 10	eqtrdi	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → 𝑋 = ( 𝑎 ∈ 1_o ↦ ( 𝑋 ‘ ∅ ) ) )
12		fconstmpt	⊢ ( 1_o × { 𝐴 } ) = ( 𝑎 ∈ 1_o ↦ 𝐴 )
13	12	a1i	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( 1_o × { 𝐴 } ) = ( 𝑎 ∈ 1_o ↦ 𝐴 ) )
14	2 3 4 11 13	ofrfval2	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( 𝑋 ∘_r ≤ ( 1_o × { 𝐴 } ) ↔ ∀ 𝑎 ∈ 1_o ( 𝑋 ‘ ∅ ) ≤ 𝐴 ) )
15		1n0	⊢ 1_o ≠ ∅
16		r19.3rzv	⊢ ( 1_o ≠ ∅ → ( ( 𝑋 ‘ ∅ ) ≤ 𝐴 ↔ ∀ 𝑎 ∈ 1_o ( 𝑋 ‘ ∅ ) ≤ 𝐴 ) )
17	15 16	mp1i	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( 𝑋 ‘ ∅ ) ≤ 𝐴 ↔ ∀ 𝑎 ∈ 1_o ( 𝑋 ‘ ∅ ) ≤ 𝐴 ) )
18		elmapi	⊢ ( 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) → 𝑋 : 1_o ⟶ ℕ₀ )
19		0lt1o	⊢ ∅ ∈ 1_o
20		ffvelcdm	⊢ ( ( 𝑋 : 1_o ⟶ ℕ₀ ∧ ∅ ∈ 1_o ) → ( 𝑋 ‘ ∅ ) ∈ ℕ₀ )
21	18 19 20	sylancl	⊢ ( 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) → ( 𝑋 ‘ ∅ ) ∈ ℕ₀ )
22	21	adantl	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( 𝑋 ‘ ∅ ) ∈ ℕ₀ )
23	22	biantrurd	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( 𝑋 ‘ ∅ ) ≤ 𝐴 ↔ ( ( 𝑋 ‘ ∅ ) ∈ ℕ₀ ∧ ( 𝑋 ‘ ∅ ) ≤ 𝐴 ) ) )
24		fznn0	⊢ ( 𝐴 ∈ ℕ₀ → ( ( 𝑋 ‘ ∅ ) ∈ ( 0 ... 𝐴 ) ↔ ( ( 𝑋 ‘ ∅ ) ∈ ℕ₀ ∧ ( 𝑋 ‘ ∅ ) ≤ 𝐴 ) ) )
25	24	adantr	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( 𝑋 ‘ ∅ ) ∈ ( 0 ... 𝐴 ) ↔ ( ( 𝑋 ‘ ∅ ) ∈ ℕ₀ ∧ ( 𝑋 ‘ ∅ ) ≤ 𝐴 ) ) )
26	23 25	bitr4d	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( 𝑋 ‘ ∅ ) ≤ 𝐴 ↔ ( 𝑋 ‘ ∅ ) ∈ ( 0 ... 𝐴 ) ) )
27	14 17 26	3bitr2d	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝑋 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( 𝑋 ∘_r ≤ ( 1_o × { 𝐴 } ) ↔ ( 𝑋 ‘ ∅ ) ∈ ( 0 ... 𝐴 ) ) )

Metamath Proof Explorer

Theorem coe1mul2lem1

Proof