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 ( 𝑥 = 𝐴𝐶 = 𝐷 )
disjprgw.2 ( 𝑥 = 𝐵𝐶 = 𝐸 )
Assertion disjprgw ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( Disj 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 ↔ ( 𝐷𝐸 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 disjprgw.1 ( 𝑥 = 𝐴𝐶 = 𝐷 )
2 disjprgw.2 ( 𝑥 = 𝐵𝐶 = 𝐸 )
3 eqeq1 ( 𝑦 = 𝐴 → ( 𝑦 = 𝑧𝐴 = 𝑧 ) )
4 nfcv 𝑥 𝐴
5 nfcv 𝑥 𝐷
6 4 5 1 csbhypf ( 𝑦 = 𝐴 𝑦 / 𝑥 𝐶 = 𝐷 )
7 6 ineq1d ( 𝑦 = 𝐴 → ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ( 𝐷 𝑧 / 𝑥 𝐶 ) )
8 7 eqeq1d ( 𝑦 = 𝐴 → ( ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ↔ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) )
9 3 8 orbi12d ( 𝑦 = 𝐴 → ( ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ) )
10 9 ralbidv ( 𝑦 = 𝐴 → ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ) )
11 eqeq1 ( 𝑦 = 𝐵 → ( 𝑦 = 𝑧𝐵 = 𝑧 ) )
12 nfcv 𝑥 𝐵
13 nfcv 𝑥 𝐸
14 12 13 2 csbhypf ( 𝑦 = 𝐵 𝑦 / 𝑥 𝐶 = 𝐸 )
15 14 ineq1d ( 𝑦 = 𝐵 → ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ( 𝐸 𝑧 / 𝑥 𝐶 ) )
16 15 eqeq1d ( 𝑦 = 𝐵 → ( ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ↔ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) )
17 11 16 orbi12d ( 𝑦 = 𝐵 → ( ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ) )
18 17 ralbidv ( 𝑦 = 𝐵 → ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ) )
19 10 18 ralprg ( ( 𝐴𝑉𝐵𝑉 ) → ( ∀ 𝑦 ∈ { 𝐴 , 𝐵 } ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ) ) )
20 19 3adant3 ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ∀ 𝑦 ∈ { 𝐴 , 𝐵 } ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ) ) )
21 id ( 𝑧 = 𝐴𝑧 = 𝐴 )
22 21 eqcomd ( 𝑧 = 𝐴𝐴 = 𝑧 )
23 22 orcd ( 𝑧 = 𝐴 → ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) )
24 trud ( 𝑧 = 𝐴 → ⊤ )
25 23 24 2thd ( 𝑧 = 𝐴 → ( ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ⊤ ) )
26 eqeq2 ( 𝑧 = 𝐵 → ( 𝐴 = 𝑧𝐴 = 𝐵 ) )
27 12 13 2 csbhypf ( 𝑧 = 𝐵 𝑧 / 𝑥 𝐶 = 𝐸 )
28 27 ineq2d ( 𝑧 = 𝐵 → ( 𝐷 𝑧 / 𝑥 𝐶 ) = ( 𝐷𝐸 ) )
29 28 eqeq1d ( 𝑧 = 𝐵 → ( ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ↔ ( 𝐷𝐸 ) = ∅ ) )
30 26 29 orbi12d ( 𝑧 = 𝐵 → ( ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ) )
31 25 30 ralprg ( ( 𝐴𝑉𝐵𝑉 ) → ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( ⊤ ∧ ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ) ) )
32 31 3adant3 ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( ⊤ ∧ ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ) ) )
33 simp3 ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → 𝐴𝐵 )
34 neneq ( 𝐴𝐵 → ¬ 𝐴 = 𝐵 )
35 biorf ( ¬ 𝐴 = 𝐵 → ( ( 𝐷𝐸 ) = ∅ ↔ ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ) )
36 33 34 35 3syl ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ( 𝐷𝐸 ) = ∅ ↔ ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ) )
37 tru
38 37 biantrur ( ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ↔ ( ⊤ ∧ ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ) )
39 36 38 bitrdi ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ( 𝐷𝐸 ) = ∅ ↔ ( ⊤ ∧ ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ) ) )
40 32 39 bitr4d ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( 𝐷𝐸 ) = ∅ ) )
41 eqeq2 ( 𝑧 = 𝐴 → ( 𝐵 = 𝑧𝐵 = 𝐴 ) )
42 eqcom ( 𝐵 = 𝐴𝐴 = 𝐵 )
43 41 42 bitrdi ( 𝑧 = 𝐴 → ( 𝐵 = 𝑧𝐴 = 𝐵 ) )
44 4 5 1 csbhypf ( 𝑧 = 𝐴 𝑧 / 𝑥 𝐶 = 𝐷 )
45 44 ineq2d ( 𝑧 = 𝐴 → ( 𝐸 𝑧 / 𝑥 𝐶 ) = ( 𝐸𝐷 ) )
46 incom ( 𝐸𝐷 ) = ( 𝐷𝐸 )
47 45 46 eqtrdi ( 𝑧 = 𝐴 → ( 𝐸 𝑧 / 𝑥 𝐶 ) = ( 𝐷𝐸 ) )
48 47 eqeq1d ( 𝑧 = 𝐴 → ( ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ↔ ( 𝐷𝐸 ) = ∅ ) )
49 43 48 orbi12d ( 𝑧 = 𝐴 → ( ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ) )
50 id ( 𝑧 = 𝐵𝑧 = 𝐵 )
51 50 eqcomd ( 𝑧 = 𝐵𝐵 = 𝑧 )
52 51 orcd ( 𝑧 = 𝐵 → ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) )
53 trud ( 𝑧 = 𝐵 → ⊤ )
54 52 53 2thd ( 𝑧 = 𝐵 → ( ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ⊤ ) )
55 49 54 ralprg ( ( 𝐴𝑉𝐵𝑉 ) → ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ∧ ⊤ ) ) )
56 55 3adant3 ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ∧ ⊤ ) ) )
57 37 biantru ( ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ↔ ( ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ∧ ⊤ ) )
58 36 57 bitrdi ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ( 𝐷𝐸 ) = ∅ ↔ ( ( 𝐴 = 𝐵 ∨ ( 𝐷𝐸 ) = ∅ ) ∧ ⊤ ) ) )
59 56 58 bitr4d ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( 𝐷𝐸 ) = ∅ ) )
60 40 59 anbi12d ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ( ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐴 = 𝑧 ∨ ( 𝐷 𝑧 / 𝑥 𝐶 ) = ∅ ) ∧ ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝐵 = 𝑧 ∨ ( 𝐸 𝑧 / 𝑥 𝐶 ) = ∅ ) ) ↔ ( ( 𝐷𝐸 ) = ∅ ∧ ( 𝐷𝐸 ) = ∅ ) ) )
61 20 60 bitrd ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( ∀ 𝑦 ∈ { 𝐴 , 𝐵 } ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ) ↔ ( ( 𝐷𝐸 ) = ∅ ∧ ( 𝐷𝐸 ) = ∅ ) ) )
62 disjors ( Disj 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 ↔ ∀ 𝑦 ∈ { 𝐴 , 𝐵 } ∀ 𝑧 ∈ { 𝐴 , 𝐵 } ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐶 𝑧 / 𝑥 𝐶 ) = ∅ ) )
63 pm4.24 ( ( 𝐷𝐸 ) = ∅ ↔ ( ( 𝐷𝐸 ) = ∅ ∧ ( 𝐷𝐸 ) = ∅ ) )
64 61 62 63 3bitr4g ( ( 𝐴𝑉𝐵𝑉𝐴𝐵 ) → ( Disj 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 ↔ ( 𝐷𝐸 ) = ∅ ) )