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 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 ↔ ( 𝐷 ∩ 𝐸 ) = ∅ ) )