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