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

Theorem mapdom2 8364
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 ((𝐴𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))

Proof of Theorem mapdom2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpr 473 . . . . . . . 8 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → 𝐶 = ∅)
21oveq1d 6883 . . . . . . 7 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶𝑚 𝐴) = (∅ ↑𝑚 𝐴))
3 simplr 776 . . . . . . . . . 10 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → ¬ (𝐴 = ∅ ∧ 𝐶 = ∅))
4 idd 24 . . . . . . . . . . 11 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐴 = ∅ → 𝐴 = ∅))
54, 1jctird 518 . . . . . . . . . 10 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐴 = ∅ → (𝐴 = ∅ ∧ 𝐶 = ∅)))
63, 5mtod 189 . . . . . . . . 9 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → ¬ 𝐴 = ∅)
76neqned 2981 . . . . . . . 8 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → 𝐴 ≠ ∅)
8 map0b 8126 . . . . . . . 8 (𝐴 ≠ ∅ → (∅ ↑𝑚 𝐴) = ∅)
97, 8syl 17 . . . . . . 7 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (∅ ↑𝑚 𝐴) = ∅)
102, 9eqtrd 2836 . . . . . 6 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶𝑚 𝐴) = ∅)
11 ovex 6900 . . . . . . 7 (𝐶𝑚 𝐵) ∈ V
12110dom 8323 . . . . . 6 ∅ ≼ (𝐶𝑚 𝐵)
1310, 12syl6eqbr 4876 . . . . 5 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
14 simpll 774 . . . . . . . 8 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → 𝐴𝐵)
15 reldom 8192 . . . . . . . . . . 11 Rel ≼
1615brrelex2i 5353 . . . . . . . . . 10 (𝐴𝐵𝐵 ∈ V)
1716ad2antrr 708 . . . . . . . . 9 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → 𝐵 ∈ V)
18 domeng 8200 . . . . . . . . 9 (𝐵 ∈ V → (𝐴𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
1917, 18syl 17 . . . . . . . 8 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (𝐴𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
2014, 19mpbid 223 . . . . . . 7 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → ∃𝑥(𝐴𝑥𝑥𝐵))
21 enrefg 8218 . . . . . . . . . . . 12 (𝐶 ∈ V → 𝐶𝐶)
2221ad2antlr 709 . . . . . . . . . . 11 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐶𝐶)
23 simprrl 790 . . . . . . . . . . 11 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐴𝑥)
24 mapen 8357 . . . . . . . . . . 11 ((𝐶𝐶𝐴𝑥) → (𝐶𝑚 𝐴) ≈ (𝐶𝑚 𝑥))
2522, 23, 24syl2anc 575 . . . . . . . . . 10 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 𝐴) ≈ (𝐶𝑚 𝑥))
26 ovexd 6902 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 𝑥) ∈ V)
27 ovexd 6902 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 (𝐵𝑥)) ∈ V)
28 simprl 778 . . . . . . . . . . . . 13 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐶 ≠ ∅)
29 simplr 776 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐶 ∈ V)
3016ad2antrr 708 . . . . . . . . . . . . . . 15 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝐵 ∈ V)
31 difexg 4997 . . . . . . . . . . . . . . 15 (𝐵 ∈ V → (𝐵𝑥) ∈ V)
3230, 31syl 17 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐵𝑥) ∈ V)
33 map0g 8127 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ V ∧ (𝐵𝑥) ∈ V) → ((𝐶𝑚 (𝐵𝑥)) = ∅ ↔ (𝐶 = ∅ ∧ (𝐵𝑥) ≠ ∅)))
34 simpl 470 . . . . . . . . . . . . . . . 16 ((𝐶 = ∅ ∧ (𝐵𝑥) ≠ ∅) → 𝐶 = ∅)
3533, 34syl6bi 244 . . . . . . . . . . . . . . 15 ((𝐶 ∈ V ∧ (𝐵𝑥) ∈ V) → ((𝐶𝑚 (𝐵𝑥)) = ∅ → 𝐶 = ∅))
3635necon3d 2995 . . . . . . . . . . . . . 14 ((𝐶 ∈ V ∧ (𝐵𝑥) ∈ V) → (𝐶 ≠ ∅ → (𝐶𝑚 (𝐵𝑥)) ≠ ∅))
3729, 32, 36syl2anc 575 . . . . . . . . . . . . 13 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶 ≠ ∅ → (𝐶𝑚 (𝐵𝑥)) ≠ ∅))
3828, 37mpd 15 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 (𝐵𝑥)) ≠ ∅)
39 xpdom3 8291 . . . . . . . . . . . 12 (((𝐶𝑚 𝑥) ∈ V ∧ (𝐶𝑚 (𝐵𝑥)) ∈ V ∧ (𝐶𝑚 (𝐵𝑥)) ≠ ∅) → (𝐶𝑚 𝑥) ≼ ((𝐶𝑚 𝑥) × (𝐶𝑚 (𝐵𝑥))))
4026, 27, 38, 39syl3anc 1483 . . . . . . . . . . 11 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 𝑥) ≼ ((𝐶𝑚 𝑥) × (𝐶𝑚 (𝐵𝑥))))
41 vex 3390 . . . . . . . . . . . . . . 15 𝑥 ∈ V
4241a1i 11 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝑥 ∈ V)
43 disjdif 4230 . . . . . . . . . . . . . . 15 (𝑥 ∩ (𝐵𝑥)) = ∅
4443a1i 11 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝑥 ∩ (𝐵𝑥)) = ∅)
45 mapunen 8362 . . . . . . . . . . . . . 14 (((𝑥 ∈ V ∧ (𝐵𝑥) ∈ V ∧ 𝐶 ∈ V) ∧ (𝑥 ∩ (𝐵𝑥)) = ∅) → (𝐶𝑚 (𝑥 ∪ (𝐵𝑥))) ≈ ((𝐶𝑚 𝑥) × (𝐶𝑚 (𝐵𝑥))))
4642, 32, 29, 44, 45syl31anc 1485 . . . . . . . . . . . . 13 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 (𝑥 ∪ (𝐵𝑥))) ≈ ((𝐶𝑚 𝑥) × (𝐶𝑚 (𝐵𝑥))))
4746ensymd 8237 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → ((𝐶𝑚 𝑥) × (𝐶𝑚 (𝐵𝑥))) ≈ (𝐶𝑚 (𝑥 ∪ (𝐵𝑥))))
48 simprrr 791 . . . . . . . . . . . . . 14 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → 𝑥𝐵)
49 undif 4239 . . . . . . . . . . . . . 14 (𝑥𝐵 ↔ (𝑥 ∪ (𝐵𝑥)) = 𝐵)
5048, 49sylib 209 . . . . . . . . . . . . 13 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝑥 ∪ (𝐵𝑥)) = 𝐵)
5150oveq2d 6884 . . . . . . . . . . . 12 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 (𝑥 ∪ (𝐵𝑥))) = (𝐶𝑚 𝐵))
5247, 51breqtrd 4863 . . . . . . . . . . 11 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → ((𝐶𝑚 𝑥) × (𝐶𝑚 (𝐵𝑥))) ≈ (𝐶𝑚 𝐵))
53 domentr 8245 . . . . . . . . . . 11 (((𝐶𝑚 𝑥) ≼ ((𝐶𝑚 𝑥) × (𝐶𝑚 (𝐵𝑥))) ∧ ((𝐶𝑚 𝑥) × (𝐶𝑚 (𝐵𝑥))) ≈ (𝐶𝑚 𝐵)) → (𝐶𝑚 𝑥) ≼ (𝐶𝑚 𝐵))
5440, 52, 53syl2anc 575 . . . . . . . . . 10 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 𝑥) ≼ (𝐶𝑚 𝐵))
55 endomtr 8244 . . . . . . . . . 10 (((𝐶𝑚 𝐴) ≈ (𝐶𝑚 𝑥) ∧ (𝐶𝑚 𝑥) ≼ (𝐶𝑚 𝐵)) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
5625, 54, 55syl2anc 575 . . . . . . . . 9 (((𝐴𝐵𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴𝑥𝑥𝐵))) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
5756expr 446 . . . . . . . 8 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → ((𝐴𝑥𝑥𝐵) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵)))
5857exlimdv 2023 . . . . . . 7 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (∃𝑥(𝐴𝑥𝑥𝐵) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵)))
5920, 58mpd 15 . . . . . 6 (((𝐴𝐵𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
6059adantlr 697 . . . . 5 ((((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 ≠ ∅) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
6113, 60pm2.61dane 3061 . . . 4 (((𝐴𝐵𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
6261an32s 634 . . 3 (((𝐴𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 ∈ V) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
6362ex 399 . 2 ((𝐴𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ∈ V → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵)))
64 reldmmap 8095 . . . 4 Rel dom ↑𝑚
6564ovprc1 6906 . . 3 𝐶 ∈ V → (𝐶𝑚 𝐴) = ∅)
6665, 12syl6eqbr 4876 . 2 𝐶 ∈ V → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
6763, 66pm2.61d1 172 1 ((𝐴𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶𝑚 𝐴) ≼ (𝐶𝑚 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wex 1859  wcel 2155  wne 2974  Vcvv 3387  cdif 3760  cun 3761  cin 3762  wss 3763  c0 4110   class class class wbr 4837   × cxp 5303  (class class class)co 6868  𝑚 cmap 8086  cen 8183  cdom 8184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-1st 7392  df-2nd 7393  df-er 7973  df-map 8088  df-en 8187  df-dom 8188
This theorem is referenced by:  mapdom3  8365  cfpwsdom  9685  hauspwdom  21512
  Copyright terms: Public domain W3C validator