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 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ 𝑥 ) ∈ V )
32 30 31 syl ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐵 ∖ 𝑥 ) ∈ V )
33 map0g ⊢ ( ( 𝐶 ∈ V ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ) → ( ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) = ∅ ↔ ( 𝐶 = ∅ ∧ ( 𝐵 ∖ 𝑥 ) ≠ ∅ ) ) )
34 simpl ⊢ ( ( 𝐶 = ∅ ∧ ( 𝐵 ∖ 𝑥 ) ≠ ∅ ) → 𝐶 = ∅ )
35 33 34 syl6bi ⊢ ( ( 𝐶 ∈ V ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ) → ( ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) = ∅ → 𝐶 = ∅ ) )
36 35 necon3d ⊢ ( ( 𝐶 ∈ V ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ) → ( 𝐶 ≠ ∅ → ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ≠ ∅ ) )
37 29 32 36 syl2anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ≠ ∅ → ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ≠ ∅ ) )
38 28 37 mpd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ≠ ∅ )
39 xpdom3 ⊢ ( ( ( 𝐶 ↑m 𝑥 ) ∈ V ∧ ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ∈ V ∧ ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ≠ ∅ ) → ( 𝐶 ↑m 𝑥 ) ≼ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) )
40 26 27 38 39 syl3anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m 𝑥 ) ≼ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) )
41 vex ⊢ 𝑥 ∈ V
42 41 a1i ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝑥 ∈ V )
43 disjdif ⊢ ( 𝑥 ∩ ( 𝐵 ∖ 𝑥 ) ) = ∅
44 43 a1i ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝑥 ∩ ( 𝐵 ∖ 𝑥 ) ) = ∅ )
45 mapunen ⊢ ( ( ( 𝑥 ∈ V ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝑥 ∩ ( 𝐵 ∖ 𝑥 ) ) = ∅ ) → ( 𝐶 ↑m ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) )
46 42 32 29 44 45 syl31anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) )
47 46 ensymd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( 𝐶 ↑m ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) ) )
48 simprrr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → 𝑥 ⊆ 𝐵 )
49 undif ⊢ ( 𝑥 ⊆ 𝐵 ↔ ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) = 𝐵 )
50 48 49 sylib ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) = 𝐵 )
51 50 oveq2d ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m ( 𝑥 ∪ ( 𝐵 ∖ 𝑥 ) ) ) = ( 𝐶 ↑m 𝐵 ) )
52 47 51 breqtrd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( 𝐶 ↑m 𝐵 ) )
53 domentr ⊢ ( ( ( 𝐶 ↑m 𝑥 ) ≼ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) ∧ ( ( 𝐶 ↑m 𝑥 ) × ( 𝐶 ↑m ( 𝐵 ∖ 𝑥 ) ) ) ≈ ( 𝐶 ↑m 𝐵 ) ) → ( 𝐶 ↑m 𝑥 ) ≼ ( 𝐶 ↑m 𝐵 ) )
54 40 52 53 syl2anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m 𝑥 ) ≼ ( 𝐶 ↑m 𝐵 ) )
55 endomtr ⊢ ( ( ( 𝐶 ↑m 𝐴 ) ≈ ( 𝐶 ↑m 𝑥 ) ∧ ( 𝐶 ↑m 𝑥 ) ≼ ( 𝐶 ↑m 𝐵 ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
56 25 54 55 syl2anc ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ( 𝐶 ≠ ∅ ∧ ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
57 56 expr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) ) )
58 57 exlimdv ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → ( ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) ) )
59 20 58 mpd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ 𝐶 ≠ ∅ ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
60 59 adantlr ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 ≠ ∅ ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
61 13 60 pm2.61dane ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V ) ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
62 61 an32s ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) ∧ 𝐶 ∈ V ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
63 62 ex ⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) → ( 𝐶 ∈ V → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) ) )
64 reldmmap ⊢ Rel dom ↑m
65 64 ovprc1 ⊢ ( ¬ 𝐶 ∈ V → ( 𝐶 ↑m 𝐴 ) = ∅ )
66 65 12 eqbrtrdi ⊢ ( ¬ 𝐶 ∈ V → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )
67 63 66 pm2.61d1 ⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ ( 𝐴 = ∅ ∧ 𝐶 = ∅ ) ) → ( 𝐶 ↑m 𝐴 ) ≼ ( 𝐶 ↑m 𝐵 ) )