Metamath Proof Explorer


Theorem disjprgw

Description: Version of disjprg with a disjoint variable condition, which does not require ax-13 . (Contributed by Gino Giotto, 26-Jan-2024)

Ref Expression
Hypotheses disjprgw.1 x=AC=D
disjprgw.2 x=BC=E
Assertion disjprgw AVBVABDisjxABCDE=

Proof

Step Hyp Ref Expression
1 disjprgw.1 x=AC=D
2 disjprgw.2 x=BC=E
3 eqeq1 y=Ay=zA=z
4 nfcv _xA
5 nfcv _xD
6 4 5 1 csbhypf y=Ay/xC=D
7 6 ineq1d y=Ay/xCz/xC=Dz/xC
8 7 eqeq1d y=Ay/xCz/xC=Dz/xC=
9 3 8 orbi12d y=Ay=zy/xCz/xC=A=zDz/xC=
10 9 ralbidv y=AzABy=zy/xCz/xC=zABA=zDz/xC=
11 eqeq1 y=By=zB=z
12 nfcv _xB
13 nfcv _xE
14 12 13 2 csbhypf y=By/xC=E
15 14 ineq1d y=By/xCz/xC=Ez/xC
16 15 eqeq1d y=By/xCz/xC=Ez/xC=
17 11 16 orbi12d y=By=zy/xCz/xC=B=zEz/xC=
18 17 ralbidv y=BzABy=zy/xCz/xC=zABB=zEz/xC=
19 10 18 ralprg AVBVyABzABy=zy/xCz/xC=zABA=zDz/xC=zABB=zEz/xC=
20 19 3adant3 AVBVAByABzABy=zy/xCz/xC=zABA=zDz/xC=zABB=zEz/xC=
21 id z=Az=A
22 21 eqcomd z=AA=z
23 22 orcd z=AA=zDz/xC=
24 trud z=A
25 23 24 2thd z=AA=zDz/xC=
26 eqeq2 z=BA=zA=B
27 12 13 2 csbhypf z=Bz/xC=E
28 27 ineq2d z=BDz/xC=DE
29 28 eqeq1d z=BDz/xC=DE=
30 26 29 orbi12d z=BA=zDz/xC=A=BDE=
31 25 30 ralprg AVBVzABA=zDz/xC=A=BDE=
32 31 3adant3 AVBVABzABA=zDz/xC=A=BDE=
33 simp3 AVBVABAB
34 neneq AB¬A=B
35 biorf ¬A=BDE=A=BDE=
36 33 34 35 3syl AVBVABDE=A=BDE=
37 tru
38 37 biantrur A=BDE=A=BDE=
39 36 38 bitrdi AVBVABDE=A=BDE=
40 32 39 bitr4d AVBVABzABA=zDz/xC=DE=
41 eqeq2 z=AB=zB=A
42 eqcom B=AA=B
43 41 42 bitrdi z=AB=zA=B
44 4 5 1 csbhypf z=Az/xC=D
45 44 ineq2d z=AEz/xC=ED
46 incom ED=DE
47 45 46 eqtrdi z=AEz/xC=DE
48 47 eqeq1d z=AEz/xC=DE=
49 43 48 orbi12d z=AB=zEz/xC=A=BDE=
50 id z=Bz=B
51 50 eqcomd z=BB=z
52 51 orcd z=BB=zEz/xC=
53 trud z=B
54 52 53 2thd z=BB=zEz/xC=
55 49 54 ralprg AVBVzABB=zEz/xC=A=BDE=
56 55 3adant3 AVBVABzABB=zEz/xC=A=BDE=
57 37 biantru A=BDE=A=BDE=
58 36 57 bitrdi AVBVABDE=A=BDE=
59 56 58 bitr4d AVBVABzABB=zEz/xC=DE=
60 40 59 anbi12d AVBVABzABA=zDz/xC=zABB=zEz/xC=DE=DE=
61 20 60 bitrd AVBVAByABzABy=zy/xCz/xC=DE=DE=
62 disjors DisjxABCyABzABy=zy/xCz/xC=
63 pm4.24 DE=DE=DE=
64 61 62 63 3bitr4g AVBVABDisjxABCDE=