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 ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑥 = 𝐴𝑦 = 𝐵 ) ) } = { 𝑥 ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑥 = 𝐴 ∨ ∃ 𝑖𝐼 𝑥 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑥 = 𝐴 ) } )

Proof

Step Hyp Ref Expression
1 rexcom4 ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑦𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) )
2 rexcom4 ( ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ↔ ∃ 𝑦𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) )
3 1 2 orbi12i ( ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ( ∃ 𝑦𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑦𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
4 19.43 ( ∃ 𝑦 ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ( ∃ 𝑦𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑦𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
5 3 4 bitr4i ( ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ∃ 𝑦 ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
6 5 rexbii ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ∃ 𝑢 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
7 rexcom4 ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ∃ 𝑦𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
8 6 7 bitri ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ∃ 𝑦𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
9 rexcom4 ( ∃ 𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑦𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) )
10 9 rexbii ( ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑢𝑆𝑦𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) )
11 rexcom4 ( ∃ 𝑢𝑆𝑦𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑦𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) )
12 10 11 bitri ( ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑦𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) )
13 8 12 orbi12i ( ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑦𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑦𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
14 19.43 ( ∃ 𝑦 ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑦𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑦𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
15 13 14 bitr4i ( ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) ↔ ∃ 𝑦 ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
16 difssd ( 𝑆𝑈 → ( 𝑈𝑆 ) ⊆ 𝑈 )
17 ssralv ( ( 𝑈𝑆 ) ⊆ 𝑈 → ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ∀ 𝑢 ∈ ( 𝑈𝑆 ) ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ) )
18 16 17 syl ( 𝑆𝑈 → ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ∀ 𝑢 ∈ ( 𝑈𝑆 ) ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ) )
19 18 impcom ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → ∀ 𝑢 ∈ ( 𝑈𝑆 ) ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) )
20 simpl ( ( 𝑧 = 𝐴𝑦 = 𝐵 ) → 𝑧 = 𝐴 )
21 20 exlimiv ( ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) → 𝑧 = 𝐴 )
22 elisset ( 𝐵𝑋 → ∃ 𝑦 𝑦 = 𝐵 )
23 ibar ( 𝑧 = 𝐴 → ( 𝑦 = 𝐵 ↔ ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
24 23 bicomd ( 𝑧 = 𝐴 → ( ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ 𝑦 = 𝐵 ) )
25 24 exbidv ( 𝑧 = 𝐴 → ( ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑦 𝑦 = 𝐵 ) )
26 22 25 syl5ibrcom ( 𝐵𝑋 → ( 𝑧 = 𝐴 → ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
27 21 26 impbid2 ( 𝐵𝑋 → ( ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ 𝑧 = 𝐴 ) )
28 27 ralrexbid ( ∀ 𝑣𝑈 𝐵𝑋 → ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑣𝑈 𝑧 = 𝐴 ) )
29 28 adantr ( ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑣𝑈 𝑧 = 𝐴 ) )
30 simpl ( ( 𝑧 = 𝐶𝑦 = 𝐷 ) → 𝑧 = 𝐶 )
31 30 exlimiv ( ∃ 𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) → 𝑧 = 𝐶 )
32 elisset ( 𝐷𝑊 → ∃ 𝑦 𝑦 = 𝐷 )
33 ibar ( 𝑧 = 𝐶 → ( 𝑦 = 𝐷 ↔ ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
34 33 bicomd ( 𝑧 = 𝐶 → ( ( 𝑧 = 𝐶𝑦 = 𝐷 ) ↔ 𝑦 = 𝐷 ) )
35 34 exbidv ( 𝑧 = 𝐶 → ( ∃ 𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ↔ ∃ 𝑦 𝑦 = 𝐷 ) )
36 32 35 syl5ibrcom ( 𝐷𝑊 → ( 𝑧 = 𝐶 → ∃ 𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
37 31 36 impbid2 ( 𝐷𝑊 → ( ∃ 𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ↔ 𝑧 = 𝐶 ) )
38 37 ralrexbid ( ∀ 𝑖𝐼 𝐷𝑊 → ( ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ↔ ∃ 𝑖𝐼 𝑧 = 𝐶 ) )
39 38 adantl ( ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ( ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ↔ ∃ 𝑖𝐼 𝑧 = 𝐶 ) )
40 29 39 orbi12d ( ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ( ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ) )
41 40 ralrexbid ( ∀ 𝑢 ∈ ( 𝑈𝑆 ) ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ) )
42 19 41 syl ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ↔ ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ) )
43 ssralv ( 𝑆𝑈 → ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ∀ 𝑢𝑆 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ) )
44 ssralv ( ( 𝑈𝑆 ) ⊆ 𝑈 → ( ∀ 𝑣𝑈 𝐵𝑋 → ∀ 𝑣 ∈ ( 𝑈𝑆 ) 𝐵𝑋 ) )
45 16 44 syl ( 𝑆𝑈 → ( ∀ 𝑣𝑈 𝐵𝑋 → ∀ 𝑣 ∈ ( 𝑈𝑆 ) 𝐵𝑋 ) )
46 45 adantrd ( 𝑆𝑈 → ( ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ∀ 𝑣 ∈ ( 𝑈𝑆 ) 𝐵𝑋 ) )
47 46 ralimdv ( 𝑆𝑈 → ( ∀ 𝑢𝑆 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ∀ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝐵𝑋 ) )
48 43 47 syld ( 𝑆𝑈 → ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) → ∀ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝐵𝑋 ) )
49 48 impcom ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → ∀ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝐵𝑋 )
50 27 ralrexbid ( ∀ 𝑣 ∈ ( 𝑈𝑆 ) 𝐵𝑋 → ( ∃ 𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑣 ∈ ( 𝑈𝑆 ) 𝑧 = 𝐴 ) )
51 50 ralrexbid ( ∀ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝐵𝑋 → ( ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑧 = 𝐴 ) )
52 49 51 syl ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → ( ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑧 = 𝐴 ) )
53 42 52 orbi12d ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → ( ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼𝑦 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ∃ 𝑦 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑧 = 𝐴 ) ) )
54 15 53 bitr3id ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → ( ∃ 𝑦 ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑧 = 𝐴 ) ) )
55 eqeq1 ( 𝑥 = 𝑧 → ( 𝑥 = 𝐴𝑧 = 𝐴 ) )
56 55 anbi1d ( 𝑥 = 𝑧 → ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) ↔ ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
57 56 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
58 eqeq1 ( 𝑥 = 𝑧 → ( 𝑥 = 𝐶𝑧 = 𝐶 ) )
59 58 anbi1d ( 𝑥 = 𝑧 → ( ( 𝑥 = 𝐶𝑦 = 𝐷 ) ↔ ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
60 59 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ↔ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) )
61 57 60 orbi12d ( 𝑥 = 𝑧 → ( ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) ↔ ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ) )
62 61 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) ↔ ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ) )
63 56 2rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑥 = 𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
64 62 63 orbi12d ( 𝑥 = 𝑧 → ( ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑥 = 𝐴𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) ) )
65 64 dmopabelb ( 𝑧 ∈ V → ( 𝑧 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑥 = 𝐴𝑦 = 𝐵 ) ) } ↔ ∃ 𝑦 ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) ) )
66 65 elv ( 𝑧 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑥 = 𝐴𝑦 = 𝐵 ) ) } ↔ ∃ 𝑦 ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑧 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑧 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑧 = 𝐴𝑦 = 𝐵 ) ) )
67 vex 𝑧 ∈ V
68 55 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑣𝑈 𝑥 = 𝐴 ↔ ∃ 𝑣𝑈 𝑧 = 𝐴 ) )
69 58 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑖𝐼 𝑥 = 𝐶 ↔ ∃ 𝑖𝐼 𝑧 = 𝐶 ) )
70 68 69 orbi12d ( 𝑥 = 𝑧 → ( ( ∃ 𝑣𝑈 𝑥 = 𝐴 ∨ ∃ 𝑖𝐼 𝑥 = 𝐶 ) ↔ ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ) )
71 70 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑥 = 𝐴 ∨ ∃ 𝑖𝐼 𝑥 = 𝐶 ) ↔ ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ) )
72 55 2rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑥 = 𝐴 ↔ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑧 = 𝐴 ) )
73 71 72 orbi12d ( 𝑥 = 𝑧 → ( ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑥 = 𝐴 ∨ ∃ 𝑖𝐼 𝑥 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑥 = 𝐴 ) ↔ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑧 = 𝐴 ) ) )
74 67 73 elab ( 𝑧 ∈ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑥 = 𝐴 ∨ ∃ 𝑖𝐼 𝑥 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑥 = 𝐴 ) } ↔ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑧 = 𝐴 ∨ ∃ 𝑖𝐼 𝑧 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑧 = 𝐴 ) )
75 54 66 74 3bitr4g ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → ( 𝑧 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑥 = 𝐴𝑦 = 𝐵 ) ) } ↔ 𝑧 ∈ { 𝑥 ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑥 = 𝐴 ∨ ∃ 𝑖𝐼 𝑥 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑥 = 𝐴 ) } ) )
76 75 eqrdv ( ( ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 𝐵𝑋 ∧ ∀ 𝑖𝐼 𝐷𝑊 ) ∧ 𝑆𝑈 ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) ( 𝑥 = 𝐴𝑦 = 𝐵 ) ) } = { 𝑥 ∣ ( ∃ 𝑢 ∈ ( 𝑈𝑆 ) ( ∃ 𝑣𝑈 𝑥 = 𝐴 ∨ ∃ 𝑖𝐼 𝑥 = 𝐶 ) ∨ ∃ 𝑢𝑆𝑣 ∈ ( 𝑈𝑆 ) 𝑥 = 𝐴 ) } )