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	⊢ ( 𝐴 ≼ 𝐵 → ( 𝐴 ↑_m 𝐶 ) ≼ ( 𝐵 ↑_m 𝐶 ) )

Proof

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

Metamath Proof Explorer

Theorem mapdom1

Proof