MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mapdom2 Structured version   Visualization version   GIF version

Theorem mapdom2 9095
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.)
Assertion
Ref Expression
mapdom2 ((𝐴𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))

Proof of Theorem mapdom2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpr 486 . . . . . . . 8 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → 𝐶 = ∅)
21oveq1d 7373 . . . . . . 7 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶m 𝐴) = (∅ ↑m 𝐴))
3 simplr 768 . . . . . . . . . 10 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → ¬ (𝐴 = ∅ ∧ 𝐶 = ∅))
4 idd 24 . . . . . . . . . . 11 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐴 = ∅ → 𝐴 = ∅))
54, 1jctird 528 . . . . . . . . . 10 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐴 = ∅ → (𝐴 = ∅ ∧ 𝐶 = ∅)))
63, 5mtod 197 . . . . . . . . 9 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → ¬ 𝐴 = ∅)
76neqned 2947 . . . . . . . 8 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → 𝐴 ≠ ∅)
8 map0b 8824 . . . . . . . 8 (𝐴 ≠ ∅ → (∅ ↑m 𝐴) = ∅)
97, 8syl 17 . . . . . . 7 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (∅ ↑m 𝐴) = ∅)
102, 9eqtrd 2773 . . . . . 6 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶m 𝐴) = ∅)
11 ovex 7391 . . . . . . 7 (𝐶m 𝐵) ∈ V
12110dom 9053 . . . . . 6 ∅ ≼ (𝐶m 𝐵)
1310, 12eqbrtrdi 5145 . . . . 5 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
14 simpll 766 . . . . . . . 8 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → 𝐴𝐵)
15 reldom 8892 . . . . . . . . . . 11 Rel ≼
1615brrelex2i 5690 . . . . . . . . . 10 (𝐴𝐵𝐵 ∈ V)
1716ad2antrr 725 . . . . . . . . 9 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → 𝐵 ∈ V)
18 domeng 8905 . . . . . . . . 9 (𝐵 ∈ V → (𝐴𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
1917, 18syl 17 . . . . . . . 8 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (𝐴𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
2014, 19mpbid 231 . . . . . . 7 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → ∃𝑥(𝐴𝑥𝑥𝐵))
21 enrefg 8927 . . . . . . . . . . . 12 (𝐶 ∈ V → 𝐶𝐶)
2221ad2antlr 726 . . . . . . . . . . 11 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐶𝐶)
23 simprrl 780 . . . . . . . . . . 11 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐴𝑥)
24 mapen 9088 . . . . . . . . . . 11 ((𝐶𝐶𝐴𝑥) → (𝐶m 𝐴) ≈ (𝐶m 𝑥))
2522, 23, 24syl2anc 585 . . . . . . . . . 10 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m 𝐴) ≈ (𝐶m 𝑥))
26 ovexd 7393 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m 𝑥) ∈ V)
27 ovexd 7393 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m (𝐵𝑥)) ∈ V)
28 simprl 770 . . . . . . . . . . . . 13 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐶 ≠ ∅)
29 simplr 768 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐶 ∈ V)
3016ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐵 ∈ V)
3130difexd 5287 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐵𝑥) ∈ V)
32 map0g 8825 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ V ∧ (𝐵𝑥) ∈ V) → ((𝐶m (𝐵𝑥)) = ∅ ↔ (𝐶 = ∅ ∧ (𝐵𝑥) ≠ ∅)))
33 simpl 484 . . . . . . . . . . . . . . . 16 ((𝐶 = ∅ ∧ (𝐵𝑥) ≠ ∅) → 𝐶 = ∅)
3432, 33syl6bi 253 . . . . . . . . . . . . . . 15 ((𝐶 ∈ V ∧ (𝐵𝑥) ∈ V) → ((𝐶m (𝐵𝑥)) = ∅ → 𝐶 = ∅))
3534necon3d 2961 . . . . . . . . . . . . . 14 ((𝐶 ∈ V ∧ (𝐵𝑥) ∈ V) → (𝐶 ≠ ∅ → (𝐶m (𝐵𝑥)) ≠ ∅))
3629, 31, 35syl2anc 585 . . . . . . . . . . . . 13 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶 ≠ ∅ → (𝐶m (𝐵𝑥)) ≠ ∅))
3728, 36mpd 15 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m (𝐵𝑥)) ≠ ∅)
38 xpdom3 9017 . . . . . . . . . . . 12 (((𝐶m 𝑥) ∈ V ∧ (𝐶m (𝐵𝑥)) ∈ V ∧ (𝐶m (𝐵𝑥)) ≠ ∅) → (𝐶m 𝑥) ≼ ((𝐶m 𝑥) × (𝐶m (𝐵𝑥))))
3926, 27, 37, 38syl3anc 1372 . . . . . . . . . . 11 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m 𝑥) ≼ ((𝐶m 𝑥) × (𝐶m (𝐵𝑥))))
40 vex 3448 . . . . . . . . . . . . . . 15 𝑥 ∈ V
4140a1i 11 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝑥 ∈ V)
42 disjdif 4432 . . . . . . . . . . . . . . 15 (𝑥 ∩ (𝐵𝑥)) = ∅
4342a1i 11 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝑥 ∩ (𝐵𝑥)) = ∅)
44 mapunen 9093 . . . . . . . . . . . . . 14 (((𝑥 ∈ V ∧ (𝐵𝑥) ∈ V ∧ 𝐶 ∈ V) ∧ (𝑥 ∩ (𝐵𝑥)) = ∅) → (𝐶m (𝑥 ∪ (𝐵𝑥))) ≈ ((𝐶m 𝑥) × (𝐶m (𝐵𝑥))))
4541, 31, 29, 43, 44syl31anc 1374 . . . . . . . . . . . . 13 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m (𝑥 ∪ (𝐵𝑥))) ≈ ((𝐶m 𝑥) × (𝐶m (𝐵𝑥))))
4645ensymd 8948 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → ((𝐶m 𝑥) × (𝐶m (𝐵𝑥))) ≈ (𝐶m (𝑥 ∪ (𝐵𝑥))))
47 simprrr 781 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝑥𝐵)
48 undif 4442 . . . . . . . . . . . . . 14 (𝑥𝐵 ↔ (𝑥 ∪ (𝐵𝑥)) = 𝐵)
4947, 48sylib 217 . . . . . . . . . . . . 13 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝑥 ∪ (𝐵𝑥)) = 𝐵)
5049oveq2d 7374 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m (𝑥 ∪ (𝐵𝑥))) = (𝐶m 𝐵))
5146, 50breqtrd 5132 . . . . . . . . . . 11 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → ((𝐶m 𝑥) × (𝐶m (𝐵𝑥))) ≈ (𝐶m 𝐵))
52 domentr 8956 . . . . . . . . . . 11 (((𝐶m 𝑥) ≼ ((𝐶m 𝑥) × (𝐶m (𝐵𝑥))) ∧ ((𝐶m 𝑥) × (𝐶m (𝐵𝑥))) ≈ (𝐶m 𝐵)) → (𝐶m 𝑥) ≼ (𝐶m 𝐵))
5339, 51, 52syl2anc 585 . . . . . . . . . 10 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m 𝑥) ≼ (𝐶m 𝐵))
54 endomtr 8955 . . . . . . . . . 10 (((𝐶m 𝐴) ≈ (𝐶m 𝑥) ∧ (𝐶m 𝑥) ≼ (𝐶m 𝐵)) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
5525, 53, 54syl2anc 585 . . . . . . . . 9 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
5655expr 458 . . . . . . . 8 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → ((𝐴𝑥𝑥𝐵) → (𝐶m 𝐴) ≼ (𝐶m 𝐵)))
5756exlimdv 1937 . . . . . . 7 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (∃𝑥(𝐴𝑥𝑥𝐵) → (𝐶m 𝐴) ≼ (𝐶m 𝐵)))
5820, 57mpd 15 . . . . . 6 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
5958adantlr 714 . . . . 5 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 ≠ ∅) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
6013, 59pm2.61dane 3029 . . . 4 (((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
6160an32s 651 . . 3 (((𝐴𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 ∈ V) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
6261ex 414 . 2 ((𝐴𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ∈ V → (𝐶m 𝐴) ≼ (𝐶m 𝐵)))
63 reldmmap 8777 . . . 4 Rel dom ↑m
6463ovprc1 7397 . . 3 𝐶 ∈ V → (𝐶m 𝐴) = ∅)
6564, 12eqbrtrdi 5145 . 2 𝐶 ∈ V → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
6662, 65pm2.61d1 180 1 ((𝐴𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶m 𝐴) ≼ (𝐶m 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107  wne 2940  Vcvv 3444  cdif 3908  cun 3909  cin 3910  wss 3911  c0 4283   class class class wbr 5106   × cxp 5632  (class class class)co 7358  m cmap 8768  cen 8883  cdom 8884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-er 8651  df-map 8770  df-en 8887  df-dom 8888
This theorem is referenced by:  mapdom3  9096  cfpwsdom  10525  hauspwdom  22868
  Copyright terms: Public domain W3C validator