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