Metamath Proof Explorer

Theorem mapdom1

Description: Order-preserving property of set exponentiation. Theorem 6L(c) of Enderton p. 149. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 9-Mar-2013)

Ref Expression
Assertion mapdom1 ⊢ A ≼ B → A C ≼ B C

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ⁡ ≼
2 1 brrelex2i ⊢ A ≼ B → B ∈ V
3 domeng ⊢ B ∈ V → A ≼ B ↔ ∃ x A ≈ x ∧ x ⊆ B
4 2 3 syl ⊢ A ≼ B → A ≼ B ↔ ∃ x A ≈ x ∧ x ⊆ B
5 4 ibi ⊢ A ≼ B → ∃ x A ≈ x ∧ x ⊆ B
6 5 adantr ⊢ A ≼ B ∧ C ∈ V → ∃ x A ≈ x ∧ x ⊆ B
7 simpl ⊢ A ≈ x ∧ x ⊆ B → A ≈ x
8 enrefg ⊢ C ∈ V → C ≈ C
9 8 adantl ⊢ A ≼ B ∧ C ∈ V → C ≈ C
10 mapen ⊢ A ≈ x ∧ C ≈ C → A C ≈ x C
11 7 9 10 syl2anr ⊢ A ≼ B ∧ C ∈ V ∧ A ≈ x ∧ x ⊆ B → A C ≈ x C
12 ovex ⊢ B C ∈ V
13 2 ad2antrr ⊢ A ≼ B ∧ C ∈ V ∧ A ≈ x ∧ x ⊆ B → B ∈ V
14 simprr ⊢ A ≼ B ∧ C ∈ V ∧ A ≈ x ∧ x ⊆ B → x ⊆ B
15 mapss ⊢ B ∈ V ∧ x ⊆ B → x C ⊆ B C
16 13 14 15 syl2anc ⊢ A ≼ B ∧ C ∈ V ∧ A ≈ x ∧ x ⊆ B → x C ⊆ B C
17 ssdomg ⊢ B C ∈ V → x C ⊆ B C → x C ≼ B C
18 12 16 17 mpsyl ⊢ A ≼ B ∧ C ∈ V ∧ A ≈ x ∧ x ⊆ B → x C ≼ B C
19 endomtr ⊢ A C ≈ x C ∧ x C ≼ B C → A C ≼ B C
20 11 18 19 syl2anc ⊢ A ≼ B ∧ C ∈ V ∧ A ≈ x ∧ x ⊆ B → A C ≼ B C
21 6 20 exlimddv ⊢ A ≼ B ∧ C ∈ V → A C ≼ B C
22 elmapex ⊢ x ∈ A C → A ∈ V ∧ C ∈ V
23 22 simprd ⊢ x ∈ A C → C ∈ V
24 23 con3i ⊢ ¬ C ∈ V → ¬ x ∈ A C
25 24 eq0rdv ⊢ ¬ C ∈ V → A C = ∅
26 25 adantl ⊢ A ≼ B ∧ ¬ C ∈ V → A C = ∅
27 12 0dom ⊢ ∅ ≼ B C
28 26 27 eqbrtrdi ⊢ A ≼ B ∧ ¬ C ∈ V → A C ≼ B C
29 21 28 pm2.61dan ⊢ A ≼ B → A C ≼ B C