Theorem mapdom3

Description: Set exponentiation dominates the mantissa. (Contributed by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 17-Jul-2022)

	Ref	Expression
Assertion	mapdom3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 )
2		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝑉 )
3		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
4	2 3	mapsnend	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ↑m { 𝑥 } ) ≈ 𝐴 )
5	4	ensymd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ≈ ( 𝐴 ↑m { 𝑥 } ) )
6		simp2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ 𝑊 )
7	3	snssd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → { 𝑥 } ⊆ 𝐵 )
8		ssdomg	⊢ ( 𝐵 ∈ 𝑊 → ( { 𝑥 } ⊆ 𝐵 → { 𝑥 } ≼ 𝐵 ) )
9	6 7 8	sylc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → { 𝑥 } ≼ 𝐵 )
10		vex	⊢ 𝑥 ∈ V
11	10	snnz	⊢ { 𝑥 } ≠ ∅
12		simpl	⊢ ( ( { 𝑥 } = ∅ ∧ 𝐴 = ∅ ) → { 𝑥 } = ∅ )
13	12	necon3ai	⊢ ( { 𝑥 } ≠ ∅ → ¬ ( { 𝑥 } = ∅ ∧ 𝐴 = ∅ ) )
14	11 13	ax-mp	⊢ ¬ ( { 𝑥 } = ∅ ∧ 𝐴 = ∅ )
15		mapdom2	⊢ ( ( { 𝑥 } ≼ 𝐵 ∧ ¬ ( { 𝑥 } = ∅ ∧ 𝐴 = ∅ ) ) → ( 𝐴 ↑m { 𝑥 } ) ≼ ( 𝐴 ↑m 𝐵 ) )
16	9 14 15	sylancl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ↑m { 𝑥 } ) ≼ ( 𝐴 ↑m 𝐵 ) )
17		endomtr	⊢ ( ( 𝐴 ≈ ( 𝐴 ↑m { 𝑥 } ) ∧ ( 𝐴 ↑m { 𝑥 } ) ≼ ( 𝐴 ↑m 𝐵 ) ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )
18	5 16 17	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )
19	18	3expia	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝐵 → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) ) )
20	19	exlimdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 𝑥 ∈ 𝐵 → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) ) )
21	1 20	syl5bi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ≠ ∅ → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) ) )
22	21	3impia	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )