Metamath Proof Explorer

Theorem coe1mul2lem1

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

Ref Expression
Assertion coe1mul2lem1 ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X ≤ f 1 𝑜 × A ↔ X ⁡ ∅ ∈ 0 … A

Proof

Step Hyp Ref Expression
1 1on ⊢ 1 𝑜 ∈ On
2 1 a1i ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → 1 𝑜 ∈ On
3 fvexd ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 ∧ a ∈ 1 𝑜 → X ⁡ ∅ ∈ V
4 simpll ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 ∧ a ∈ 1 𝑜 → A ∈ ℕ 0
5 df1o2 ⊢ 1 𝑜 = ∅
6 nn0ex ⊢ ℕ 0 ∈ V
7 0ex ⊢ ∅ ∈ V
8 5 6 7 mapsnconst ⊢ X ∈ ℕ 0 1 𝑜 → X = 1 𝑜 × X ⁡ ∅
9 8 adantl ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X = 1 𝑜 × X ⁡ ∅
10 fconstmpt ⊢ 1 𝑜 × X ⁡ ∅ = a ∈ 1 𝑜 ⟼ X ⁡ ∅
11 9 10 eqtrdi ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X = a ∈ 1 𝑜 ⟼ X ⁡ ∅
12 fconstmpt ⊢ 1 𝑜 × A = a ∈ 1 𝑜 ⟼ A
13 12 a1i ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → 1 𝑜 × A = a ∈ 1 𝑜 ⟼ A
14 2 3 4 11 13 ofrfval2 ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X ≤ f 1 𝑜 × A ↔ ∀ a ∈ 1 𝑜 X ⁡ ∅ ≤ A
15 1n0 ⊢ 1 𝑜 ≠ ∅
16 r19.3rzv ⊢ 1 𝑜 ≠ ∅ → X ⁡ ∅ ≤ A ↔ ∀ a ∈ 1 𝑜 X ⁡ ∅ ≤ A
17 15 16 mp1i ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X ⁡ ∅ ≤ A ↔ ∀ a ∈ 1 𝑜 X ⁡ ∅ ≤ A
18 elmapi ⊢ X ∈ ℕ 0 1 𝑜 → X : 1 𝑜 ⟶ ℕ 0
19 0lt1o ⊢ ∅ ∈ 1 𝑜
20 ffvelrn ⊢ X : 1 𝑜 ⟶ ℕ 0 ∧ ∅ ∈ 1 𝑜 → X ⁡ ∅ ∈ ℕ 0
21 18 19 20 sylancl ⊢ X ∈ ℕ 0 1 𝑜 → X ⁡ ∅ ∈ ℕ 0
22 21 adantl ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X ⁡ ∅ ∈ ℕ 0
23 22 biantrurd ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X ⁡ ∅ ≤ A ↔ X ⁡ ∅ ∈ ℕ 0 ∧ X ⁡ ∅ ≤ A
24 fznn0 ⊢ A ∈ ℕ 0 → X ⁡ ∅ ∈ 0 … A ↔ X ⁡ ∅ ∈ ℕ 0 ∧ X ⁡ ∅ ≤ A
25 24 adantr ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X ⁡ ∅ ∈ 0 … A ↔ X ⁡ ∅ ∈ ℕ 0 ∧ X ⁡ ∅ ≤ A
26 23 25 bitr4d ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X ⁡ ∅ ≤ A ↔ X ⁡ ∅ ∈ 0 … A
27 14 17 26 3bitr2d ⊢ A ∈ ℕ 0 ∧ X ∈ ℕ 0 1 𝑜 → X ≤ f 1 𝑜 × A ↔ X ⁡ ∅ ∈ 0 … A