Metamath Proof Explorer

Theorem dmopab3rexdif

Description: The domain of an ordered pair class abstraction with three nested restricted existential quantifiers with differences. (Contributed by AV, 25-Oct-2023)

Ref Expression
Assertion dmopab3rexdif ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → dom ⁡ x y | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A ∧ y = B = x | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∨ ∃ i ∈ I x = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ∃ v ∈ U ∃ y z = A ∧ y = B ↔ ∃ y ∃ v ∈ U z = A ∧ y = B
2 rexcom4 ⊢ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ y ∃ i ∈ I z = C ∧ y = D
3 1 2 orbi12i ⊢ ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ y ∃ v ∈ U z = A ∧ y = B ∨ ∃ y ∃ i ∈ I z = C ∧ y = D
4 19.43 ⊢ ∃ y ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ↔ ∃ y ∃ v ∈ U z = A ∧ y = B ∨ ∃ y ∃ i ∈ I z = C ∧ y = D
5 3 4 bitr4i ⊢ ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ y ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
6 5 rexbii ⊢ ∃ u ∈ U ∖ S ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ u ∈ U ∖ S ∃ y ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
7 rexcom4 ⊢ ∃ u ∈ U ∖ S ∃ y ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ↔ ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
8 6 7 bitri ⊢ ∃ u ∈ U ∖ S ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
9 rexcom4 ⊢ ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ y ∃ v ∈ U ∖ S z = A ∧ y = B
10 9 rexbii ⊢ ∃ u ∈ S ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ u ∈ S ∃ y ∃ v ∈ U ∖ S z = A ∧ y = B
11 rexcom4 ⊢ ∃ u ∈ S ∃ y ∃ v ∈ U ∖ S z = A ∧ y = B ↔ ∃ y ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
12 10 11 bitri ⊢ ∃ u ∈ S ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ y ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
13 8 12 orbi12i ⊢ ∃ u ∈ U ∖ S ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ∨ ∃ y ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
14 19.43 ⊢ ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B ↔ ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ∨ ∃ y ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
15 13 14 bitr4i ⊢ ∃ u ∈ U ∖ S ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
16 difssd ⊢ S ⊆ U → U ∖ S ⊆ U
17 ssralv ⊢ U ∖ S ⊆ U → ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∀ u ∈ U ∖ S ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W
18 16 17 syl ⊢ S ⊆ U → ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∀ u ∈ U ∖ S ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W
19 18 impcom ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → ∀ u ∈ U ∖ S ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W
20 simpl ⊢ z = A ∧ y = B → z = A
21 20 exlimiv ⊢ ∃ y z = A ∧ y = B → z = A
22 elisset ⊢ B ∈ X → ∃ y y = B
23 ibar ⊢ z = A → y = B ↔ z = A ∧ y = B
24 23 bicomd ⊢ z = A → z = A ∧ y = B ↔ y = B
25 24 exbidv ⊢ z = A → ∃ y z = A ∧ y = B ↔ ∃ y y = B
26 22 25 syl5ibrcom ⊢ B ∈ X → z = A → ∃ y z = A ∧ y = B
27 21 26 impbid2 ⊢ B ∈ X → ∃ y z = A ∧ y = B ↔ z = A
28 27 ralrexbid ⊢ ∀ v ∈ U B ∈ X → ∃ v ∈ U ∃ y z = A ∧ y = B ↔ ∃ v ∈ U z = A
29 28 adantr ⊢ ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ v ∈ U ∃ y z = A ∧ y = B ↔ ∃ v ∈ U z = A
30 simpl ⊢ z = C ∧ y = D → z = C
31 30 exlimiv ⊢ ∃ y z = C ∧ y = D → z = C
32 elisset ⊢ D ∈ W → ∃ y y = D
33 ibar ⊢ z = C → y = D ↔ z = C ∧ y = D
34 33 bicomd ⊢ z = C → z = C ∧ y = D ↔ y = D
35 34 exbidv ⊢ z = C → ∃ y z = C ∧ y = D ↔ ∃ y y = D
36 32 35 syl5ibrcom ⊢ D ∈ W → z = C → ∃ y z = C ∧ y = D
37 31 36 impbid2 ⊢ D ∈ W → ∃ y z = C ∧ y = D ↔ z = C
38 37 ralrexbid ⊢ ∀ i ∈ I D ∈ W → ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ i ∈ I z = C
39 38 adantl ⊢ ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ i ∈ I z = C
40 29 39 orbi12d ⊢ ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C
41 40 ralrexbid ⊢ ∀ u ∈ U ∖ S ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ u ∈ U ∖ S ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C
42 19 41 syl ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → ∃ u ∈ U ∖ S ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C
43 ssralv ⊢ S ⊆ U → ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∀ u ∈ S ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W
44 ssralv ⊢ U ∖ S ⊆ U → ∀ v ∈ U B ∈ X → ∀ v ∈ U ∖ S B ∈ X
45 16 44 syl ⊢ S ⊆ U → ∀ v ∈ U B ∈ X → ∀ v ∈ U ∖ S B ∈ X
46 45 adantrd ⊢ S ⊆ U → ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∀ v ∈ U ∖ S B ∈ X
47 46 ralimdv ⊢ S ⊆ U → ∀ u ∈ S ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∀ u ∈ S ∀ v ∈ U ∖ S B ∈ X
48 43 47 syld ⊢ S ⊆ U → ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W → ∀ u ∈ S ∀ v ∈ U ∖ S B ∈ X
49 48 impcom ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → ∀ u ∈ S ∀ v ∈ U ∖ S B ∈ X
50 27 ralrexbid ⊢ ∀ v ∈ U ∖ S B ∈ X → ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ v ∈ U ∖ S z = A
51 50 ralrexbid ⊢ ∀ u ∈ S ∀ v ∈ U ∖ S B ∈ X → ∃ u ∈ S ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ u ∈ S ∃ v ∈ U ∖ S z = A
52 49 51 syl ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → ∃ u ∈ S ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ u ∈ S ∃ v ∈ U ∖ S z = A
53 42 52 orbi12d ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → ∃ u ∈ U ∖ S ∃ v ∈ U ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S ∃ y z = A ∧ y = B ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A
54 15 53 bitr3id ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A
55 eqeq1 ⊢ x = z → x = A ↔ z = A
56 55 anbi1d ⊢ x = z → x = A ∧ y = B ↔ z = A ∧ y = B
57 56 rexbidv ⊢ x = z → ∃ v ∈ U x = A ∧ y = B ↔ ∃ v ∈ U z = A ∧ y = B
58 eqeq1 ⊢ x = z → x = C ↔ z = C
59 58 anbi1d ⊢ x = z → x = C ∧ y = D ↔ z = C ∧ y = D
60 59 rexbidv ⊢ x = z → ∃ i ∈ I x = C ∧ y = D ↔ ∃ i ∈ I z = C ∧ y = D
61 57 60 orbi12d ⊢ x = z → ∃ v ∈ U x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ↔ ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
62 61 rexbidv ⊢ x = z → ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
63 56 2rexbidv ⊢ x = z → ∃ u ∈ S ∃ v ∈ U ∖ S x = A ∧ y = B ↔ ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
64 62 63 orbi12d ⊢ x = z → ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A ∧ y = B ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
65 64 dmopabelb ⊢ z ∈ V → z ∈ dom ⁡ x y | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A ∧ y = B ↔ ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
66 65 elv ⊢ z ∈ dom ⁡ x y | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A ∧ y = B ↔ ∃ y ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A ∧ y = B
67 vex ⊢ z ∈ V
68 55 rexbidv ⊢ x = z → ∃ v ∈ U x = A ↔ ∃ v ∈ U z = A
69 58 rexbidv ⊢ x = z → ∃ i ∈ I x = C ↔ ∃ i ∈ I z = C
70 68 69 orbi12d ⊢ x = z → ∃ v ∈ U x = A ∨ ∃ i ∈ I x = C ↔ ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C
71 70 rexbidv ⊢ x = z → ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∨ ∃ i ∈ I x = C ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C
72 55 2rexbidv ⊢ x = z → ∃ u ∈ S ∃ v ∈ U ∖ S x = A ↔ ∃ u ∈ S ∃ v ∈ U ∖ S z = A
73 71 72 orbi12d ⊢ x = z → ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∨ ∃ i ∈ I x = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A
74 67 73 elab ⊢ z ∈ x | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∨ ∃ i ∈ I x = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A ↔ ∃ u ∈ U ∖ S ∃ v ∈ U z = A ∨ ∃ i ∈ I z = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S z = A
75 54 66 74 3bitr4g ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → z ∈ dom ⁡ x y | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A ∧ y = B ↔ z ∈ x | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∨ ∃ i ∈ I x = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A
76 75 eqrdv ⊢ ∀ u ∈ U ∀ v ∈ U B ∈ X ∧ ∀ i ∈ I D ∈ W ∧ S ⊆ U → dom ⁡ x y | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A ∧ y = B = x | ∃ u ∈ U ∖ S ∃ v ∈ U x = A ∨ ∃ i ∈ I x = C ∨ ∃ u ∈ S ∃ v ∈ U ∖ S x = A