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

Theorem undom 8597
Description: Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257. (Contributed by NM, 3-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
undom (((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) → (𝐴𝐶) ≼ (𝐵𝐷))

Proof of Theorem undom
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 8507 . . . . . . 7 Rel ≼
21brrelex2i 5602 . . . . . 6 (𝐴𝐵𝐵 ∈ V)
3 domeng 8515 . . . . . 6 (𝐵 ∈ V → (𝐴𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
42, 3syl 17 . . . . 5 (𝐴𝐵 → (𝐴𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
54ibi 269 . . . 4 (𝐴𝐵 → ∃𝑥(𝐴𝑥𝑥𝐵))
61brrelex1i 5601 . . . . . . 7 (𝐶𝐷𝐶 ∈ V)
7 difss 4106 . . . . . . 7 (𝐶𝐴) ⊆ 𝐶
8 ssdomg 8547 . . . . . . 7 (𝐶 ∈ V → ((𝐶𝐴) ⊆ 𝐶 → (𝐶𝐴) ≼ 𝐶))
96, 7, 8mpisyl 21 . . . . . 6 (𝐶𝐷 → (𝐶𝐴) ≼ 𝐶)
10 domtr 8554 . . . . . 6 (((𝐶𝐴) ≼ 𝐶𝐶𝐷) → (𝐶𝐴) ≼ 𝐷)
119, 10mpancom 686 . . . . 5 (𝐶𝐷 → (𝐶𝐴) ≼ 𝐷)
121brrelex2i 5602 . . . . . . 7 ((𝐶𝐴) ≼ 𝐷𝐷 ∈ V)
13 domeng 8515 . . . . . . 7 (𝐷 ∈ V → ((𝐶𝐴) ≼ 𝐷 ↔ ∃𝑦((𝐶𝐴) ≈ 𝑦𝑦𝐷)))
1412, 13syl 17 . . . . . 6 ((𝐶𝐴) ≼ 𝐷 → ((𝐶𝐴) ≼ 𝐷 ↔ ∃𝑦((𝐶𝐴) ≈ 𝑦𝑦𝐷)))
1514ibi 269 . . . . 5 ((𝐶𝐴) ≼ 𝐷 → ∃𝑦((𝐶𝐴) ≈ 𝑦𝑦𝐷))
1611, 15syl 17 . . . 4 (𝐶𝐷 → ∃𝑦((𝐶𝐴) ≈ 𝑦𝑦𝐷))
175, 16anim12i 614 . . 3 ((𝐴𝐵𝐶𝐷) → (∃𝑥(𝐴𝑥𝑥𝐵) ∧ ∃𝑦((𝐶𝐴) ≈ 𝑦𝑦𝐷)))
1817adantr 483 . 2 (((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) → (∃𝑥(𝐴𝑥𝑥𝐵) ∧ ∃𝑦((𝐶𝐴) ≈ 𝑦𝑦𝐷)))
19 exdistrv 1950 . . 3 (∃𝑥𝑦((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷)) ↔ (∃𝑥(𝐴𝑥𝑥𝐵) ∧ ∃𝑦((𝐶𝐴) ≈ 𝑦𝑦𝐷)))
20 simprll 777 . . . . . . 7 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → 𝐴𝑥)
21 simprrl 779 . . . . . . 7 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝐶𝐴) ≈ 𝑦)
22 disjdif 4419 . . . . . . . 8 (𝐴 ∩ (𝐶𝐴)) = ∅
2322a1i 11 . . . . . . 7 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝐴 ∩ (𝐶𝐴)) = ∅)
24 ss2in 4211 . . . . . . . . . 10 ((𝑥𝐵𝑦𝐷) → (𝑥𝑦) ⊆ (𝐵𝐷))
2524ad2ant2l 744 . . . . . . . . 9 (((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷)) → (𝑥𝑦) ⊆ (𝐵𝐷))
2625adantl 484 . . . . . . . 8 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝑥𝑦) ⊆ (𝐵𝐷))
27 simplr 767 . . . . . . . 8 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝐵𝐷) = ∅)
28 sseq0 4351 . . . . . . . 8 (((𝑥𝑦) ⊆ (𝐵𝐷) ∧ (𝐵𝐷) = ∅) → (𝑥𝑦) = ∅)
2926, 27, 28syl2anc 586 . . . . . . 7 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝑥𝑦) = ∅)
30 undif2 4423 . . . . . . . 8 (𝐴 ∪ (𝐶𝐴)) = (𝐴𝐶)
31 unen 8588 . . . . . . . 8 (((𝐴𝑥 ∧ (𝐶𝐴) ≈ 𝑦) ∧ ((𝐴 ∩ (𝐶𝐴)) = ∅ ∧ (𝑥𝑦) = ∅)) → (𝐴 ∪ (𝐶𝐴)) ≈ (𝑥𝑦))
3230, 31eqbrtrrid 5093 . . . . . . 7 (((𝐴𝑥 ∧ (𝐶𝐴) ≈ 𝑦) ∧ ((𝐴 ∩ (𝐶𝐴)) = ∅ ∧ (𝑥𝑦) = ∅)) → (𝐴𝐶) ≈ (𝑥𝑦))
3320, 21, 23, 29, 32syl22anc 836 . . . . . 6 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝐴𝐶) ≈ (𝑥𝑦))
342ad3antrrr 728 . . . . . . . 8 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → 𝐵 ∈ V)
351brrelex2i 5602 . . . . . . . . 9 (𝐶𝐷𝐷 ∈ V)
3635ad3antlr 729 . . . . . . . 8 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → 𝐷 ∈ V)
37 unexg 7464 . . . . . . . 8 ((𝐵 ∈ V ∧ 𝐷 ∈ V) → (𝐵𝐷) ∈ V)
3834, 36, 37syl2anc 586 . . . . . . 7 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝐵𝐷) ∈ V)
39 unss12 4156 . . . . . . . . 9 ((𝑥𝐵𝑦𝐷) → (𝑥𝑦) ⊆ (𝐵𝐷))
4039ad2ant2l 744 . . . . . . . 8 (((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷)) → (𝑥𝑦) ⊆ (𝐵𝐷))
4140adantl 484 . . . . . . 7 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝑥𝑦) ⊆ (𝐵𝐷))
42 ssdomg 8547 . . . . . . 7 ((𝐵𝐷) ∈ V → ((𝑥𝑦) ⊆ (𝐵𝐷) → (𝑥𝑦) ≼ (𝐵𝐷)))
4338, 41, 42sylc 65 . . . . . 6 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝑥𝑦) ≼ (𝐵𝐷))
44 endomtr 8559 . . . . . 6 (((𝐴𝐶) ≈ (𝑥𝑦) ∧ (𝑥𝑦) ≼ (𝐵𝐷)) → (𝐴𝐶) ≼ (𝐵𝐷))
4533, 43, 44syl2anc 586 . . . . 5 ((((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) ∧ ((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷))) → (𝐴𝐶) ≼ (𝐵𝐷))
4645ex 415 . . . 4 (((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) → (((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷)) → (𝐴𝐶) ≼ (𝐵𝐷)))
4746exlimdvv 1929 . . 3 (((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) → (∃𝑥𝑦((𝐴𝑥𝑥𝐵) ∧ ((𝐶𝐴) ≈ 𝑦𝑦𝐷)) → (𝐴𝐶) ≼ (𝐵𝐷)))
4819, 47syl5bir 245 . 2 (((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) → ((∃𝑥(𝐴𝑥𝑥𝐵) ∧ ∃𝑦((𝐶𝐴) ≈ 𝑦𝑦𝐷)) → (𝐴𝐶) ≼ (𝐵𝐷)))
4918, 48mpd 15 1 (((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) → (𝐴𝐶) ≼ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1531  wex 1774  wcel 2108  Vcvv 3493  cdif 3931  cun 3932  cin 3933  wss 3934  c0 4289   class class class wbr 5057  cen 8498  cdom 8499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-en 8502  df-dom 8503
This theorem is referenced by:  domunsncan  8609  domunsn  8659  sucdom2  8706  unxpdom2  8718  sucxpdom  8719  fodomfi  8789  undjudom  9585  djudom1  9600
  Copyright terms: Public domain W3C validator