Metamath Proof Explorer

Theorem mapdom2

Description: Order-preserving property of set exponentiation. Theorem 6L(d) of Enderton p. 149. (Contributed by NM, 23-Sep-2004) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion mapdom2 ( ( 𝐴 ≼ 𝐵 ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → 𝐶 = ∅ )
2 1 oveq1d ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → ( 𝐶 ↑m 𝐴 ) = ( ∅ ↑m 𝐴 ) )
3 simplr ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) )
4 idd ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → ( 𝐴 = ∅ → 𝐴 = ∅ ) )
5 4 1 jctird ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → ( 𝐴 = ∅ → ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) )
6 3 5 mtod ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → ¬ 𝐴 = ∅ )
7 6 neqned ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → 𝐴 ≠ ∅ )
8 map0b ⊢ ( 𝐴 ≠ ∅ → ( ∅ ↑m 𝐴 ) = ∅ )
9 7 8 syl ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → ( ∅ ↑m 𝐴 ) = ∅ )
10 2 9 eqtrd ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → ( 𝐶 ↑m 𝐴 ) = ∅ )
11 ovex ⊢ ( 𝐶 ↑m 𝐵 ) ∈ V
12 11 0dom ⊢ ∅ ≼ ( 𝐶 ↑m 𝐵 )
13 10 12 eqbrtrdi ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 = ∅ ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
14 simpll ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → 𝐴 ≼ 𝐵 )
15 reldom ⊢ Rel ≼
16 15 brrelex2i ⊢ ( 𝐴 ≼ 𝐵 → 𝐵 ∈ V )
17 16 ad2antrr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → 𝐵 ∈ V )
18 domeng ⊢ ( 𝐵 ∈ V → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) )
19 17 18 syl ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) )
20 14 19 mpbid ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
21 enrefg ⊢ ( 𝐶 ∈ V → 𝐶 ≈ 𝐶 )
22 21 ad2antlr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝐶 ≈ 𝐶 )
23 simprrl ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝐴 ≈ 𝑥 )
24 mapen ⊢ ( ( 𝐶 ≈ 𝐶 ∧ 𝐴 ≈ 𝑥 ) → ( 𝐶 ↑m 𝐴 ) ≈ ( 𝐶 ↑m 𝑥 ) )
25 22 23 24 syl2anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m 𝐴 ) ≈ ( 𝐶 ↑m 𝑥 ) )
26 ovexd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m 𝑥 ) ∈ V )
27 ovexd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ∈ V )
28 simprl ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝐶 ≠ ∅ )
29 simplr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝐶 ∈ V )
30 16 ad2antrr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝐵 ∈ V )
31 30 difexd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐵 ∖ 𝑥 ) ∈ V )
32 map0g ⊢ ( ( 𝐶 ∈ V ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ) → ( ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) = ∅ ↔ ( 𝐶 = ∅ ∧ ( 𝐵 ∖ 𝑥 ) ≠ ∅ ) ) )
33 simpl ⊢ ( ( 𝐶 = ∅ ∧ ( 𝐵 ∖ 𝑥 ) ≠ ∅ ) → 𝐶 = ∅ )
34 32 33 syl6bi ⊢ ( ( 𝐶 ∈ V ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ) → ( ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) = ∅ → 𝐶 = ∅ ) )
35 34 necon3d ⊢ ( ( 𝐶 ∈ V ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ) → ( 𝐶 ≠ ∅ → ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ≠ ∅ ) )
36 29 31 35 syl2anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ≠ ∅ → ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ≠ ∅ ) )
37 28 36 mpd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ≠ ∅ )
38 xpdom3 ⊢ ( ( ( 𝐶 ↑m 𝑥 ) ∈ V ∧ ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ∈ V ∧ ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ≠ ∅ ) → ( 𝐶 ↑m 𝑥 ) ≼ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) )
39 26 27 37 38 syl3anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m 𝑥 ) ≼ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) )
40 vex ⊢ 𝑥 ∈ V
41 40 a1i ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝑥 ∈ V )
42 disjdif ⊢ ( 𝑥 ∩ ( 𝐵 ∖ 𝑥 ) ) = ∅
43 42 a1i ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝑥 ∩ ( 𝐵 ∖ 𝑥 ) ) = ∅ )
44 mapunen ⊢ ( ( ( 𝑥 ∈ V ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝑥 ∩ ( 𝐵 ∖ 𝑥 ) ) = ∅ ) → ( 𝐶 ↑m ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) )
45 41 31 29 43 44 syl31anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) )
46 45 ensymd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( 𝐶 ↑m ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) ) )
47 simprrr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝑥 ⊆ 𝐵 )
48 undif ⊢ ( 𝑥 ⊆ 𝐵 ↔ ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) = 𝐵 )
49 47 48 sylib ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) = 𝐵 )
50 49 oveq2d ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) ) = ( 𝐶 ↑m 𝐵 ) )
51 46 50 breqtrd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( 𝐶 ↑m 𝐵 ) )
52 domentr ⊢ ( ( ( 𝐶 ↑m 𝑥 ) ≼ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) ∧ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( 𝐶 ↑m 𝐵 ) ) → ( 𝐶 ↑m 𝑥 ) ≼ ( 𝐶 ↑m 𝐵 ) )
53 39 51 52 syl2anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m 𝑥 ) ≼ ( 𝐶 ↑m 𝐵 ) )
54 endomtr ⊢ ( ( ( 𝐶 ↑m 𝐴 ) ≈ ( 𝐶 ↑m 𝑥 ) ∧ ( 𝐶 ↑m 𝑥 ) ≼ ( 𝐶 ↑m 𝐵 ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
55 25 53 54 syl2anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
56 55 expr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) ) )
57 56 exlimdv ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → ( ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) ) )
58 20 57 mpd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
59 58 adantlr ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 ≠ ∅ ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
60 13 59 pm2.61dane ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
61 60 an32s ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 ∈ V ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
62 61 ex ⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) → ( 𝐶 ∈ V → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) ) )
63 reldmmap ⊢ Rel dom ↑m
64 63 ovprc1 ⊢ ( ¬ 𝐶 ∈ V → ( 𝐶 ↑m 𝐴 ) = ∅ )
65 64 12 eqbrtrdi ⊢ ( ¬ 𝐶 ∈ V → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
66 62 65 pm2.61d1 ⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )