Step |
Hyp |
Ref |
Expression |
1 |
|
fiun.1 |
⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 ) |
2 |
|
vex |
⊢ 𝑣 ∈ V |
3 |
|
eqeq1 |
⊢ ( 𝑧 = 𝑣 → ( 𝑧 = 𝐵 ↔ 𝑣 = 𝐵 ) ) |
4 |
3
|
rexbidv |
⊢ ( 𝑧 = 𝑣 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑣 = 𝐵 ) ) |
5 |
2 4
|
elab |
⊢ ( 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑣 = 𝐵 ) |
6 |
1
|
eqeq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝑣 = 𝐵 ↔ 𝑣 = 𝐶 ) ) |
7 |
6
|
cbvrexvw |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝑣 = 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑣 = 𝐶 ) |
8 |
|
r19.29 |
⊢ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑣 = 𝐶 ) → ∃ 𝑦 ∈ 𝐴 ( ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ∧ 𝑣 = 𝐶 ) ) |
9 |
|
sseq12 |
⊢ ( ( 𝑢 = 𝐵 ∧ 𝑣 = 𝐶 ) → ( 𝑢 ⊆ 𝑣 ↔ 𝐵 ⊆ 𝐶 ) ) |
10 |
9
|
ancoms |
⊢ ( ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐵 ) → ( 𝑢 ⊆ 𝑣 ↔ 𝐵 ⊆ 𝐶 ) ) |
11 |
|
sseq12 |
⊢ ( ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐵 ) → ( 𝑣 ⊆ 𝑢 ↔ 𝐶 ⊆ 𝐵 ) ) |
12 |
10 11
|
orbi12d |
⊢ ( ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐵 ) → ( ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ↔ ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ) |
13 |
12
|
biimprcd |
⊢ ( ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) → ( ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐵 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) |
14 |
13
|
expdimp |
⊢ ( ( ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ∧ 𝑣 = 𝐶 ) → ( 𝑢 = 𝐵 → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) |
15 |
14
|
rexlimivw |
⊢ ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ∧ 𝑣 = 𝐶 ) → ( 𝑢 = 𝐵 → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) |
16 |
15
|
imp |
⊢ ( ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ∧ 𝑣 = 𝐶 ) ∧ 𝑢 = 𝐵 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) |
17 |
8 16
|
sylan |
⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑣 = 𝐶 ) ∧ 𝑢 = 𝐵 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) |
18 |
17
|
an32s |
⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑣 = 𝐶 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) |
19 |
18
|
adantlll |
⊢ ( ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑣 = 𝐶 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) |
20 |
7 19
|
sylan2b |
⊢ ( ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑣 = 𝐵 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) |
21 |
5 20
|
sylan2b |
⊢ ( ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) ∧ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) |
22 |
21
|
ralrimiva |
⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) |