Metamath Proof Explorer


Theorem undom

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) Avoid ax-pow . (Revised by BTernaryTau, 4-Dec-2024)

Ref Expression
Assertion undom A B C D B D = A C B D

Proof

Step Hyp Ref Expression
1 undif2 A C A = A C
2 reldom Rel
3 2 brrelex2i A B B V
4 2 brrelex2i C D D V
5 unexg B V D V B D V
6 3 4 5 syl2an A B C D B D V
7 6 adantr A B C D B D = B D V
8 brdomi A B x x : A 1-1 B
9 brdomi C D y y : C 1-1 D
10 exdistrv x y x : A 1-1 B y : C 1-1 D x x : A 1-1 B y y : C 1-1 D
11 disjdif A C A =
12 difss C A C
13 f1ssres y : C 1-1 D C A C y C A : C A 1-1 D
14 12 13 mpan2 y : C 1-1 D y C A : C A 1-1 D
15 f1un x : A 1-1 B y C A : C A 1-1 D A C A = B D = x y C A : A C A 1-1 B D
16 14 15 sylanl2 x : A 1-1 B y : C 1-1 D A C A = B D = x y C A : A C A 1-1 B D
17 11 16 mpanr1 x : A 1-1 B y : C 1-1 D B D = x y C A : A C A 1-1 B D
18 vex x V
19 vex y V
20 19 resex y C A V
21 18 20 unex x y C A V
22 f1dom3g x y C A V B D V x y C A : A C A 1-1 B D A C A B D
23 21 22 mp3an1 B D V x y C A : A C A 1-1 B D A C A B D
24 23 expcom x y C A : A C A 1-1 B D B D V A C A B D
25 17 24 syl x : A 1-1 B y : C 1-1 D B D = B D V A C A B D
26 25 ex x : A 1-1 B y : C 1-1 D B D = B D V A C A B D
27 26 exlimivv x y x : A 1-1 B y : C 1-1 D B D = B D V A C A B D
28 10 27 sylbir x x : A 1-1 B y y : C 1-1 D B D = B D V A C A B D
29 8 9 28 syl2an A B C D B D = B D V A C A B D
30 29 imp A B C D B D = B D V A C A B D
31 7 30 mpd A B C D B D = A C A B D
32 1 31 eqbrtrrid A B C D B D = A C B D