Theorem coe1mul2lem1

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

	Ref	Expression
Assertion	coe1mul2lem1	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑋 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑋 ∘r ≤ ( 1o × { 𝐴 } ) ↔ ( 𝑋 ‘ ∅ ) ∈ ( 0 ... 𝐴 ) ) )

Proof

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