Step |
Hyp |
Ref |
Expression |
1 |
|
hsmexlem.f |
⊢ 𝐹 = OrdIso ( E , 𝐵 ) |
2 |
|
hsmexlem.g |
⊢ 𝐺 = OrdIso ( E , ∪ 𝑎 ∈ 𝐴 𝐵 ) |
3 |
|
wdomref |
⊢ ( 𝐶 ∈ On → 𝐶 ≼* 𝐶 ) |
4 |
|
xpwdomg |
⊢ ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ≼* 𝐶 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐷 × 𝐶 ) ) |
5 |
3 4
|
sylan2 |
⊢ ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐷 × 𝐶 ) ) |
6 |
|
wdompwdom |
⊢ ( ( 𝐴 × 𝐶 ) ≼* ( 𝐷 × 𝐶 ) → 𝒫 ( 𝐴 × 𝐶 ) ≼ 𝒫 ( 𝐷 × 𝐶 ) ) |
7 |
|
harword |
⊢ ( 𝒫 ( 𝐴 × 𝐶 ) ≼ 𝒫 ( 𝐷 × 𝐶 ) → ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) ⊆ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) ) |
8 |
5 6 7
|
3syl |
⊢ ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) → ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) ⊆ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) ⊆ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) ) |
10 |
|
relwdom |
⊢ Rel ≼* |
11 |
10
|
brrelex1i |
⊢ ( 𝐴 ≼* 𝐷 → 𝐴 ∈ V ) |
12 |
11
|
adantr |
⊢ ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) → 𝐴 ∈ V ) |
13 |
12
|
adantr |
⊢ ( ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → 𝐴 ∈ V ) |
14 |
|
simplr |
⊢ ( ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → 𝐶 ∈ On ) |
15 |
|
simpr |
⊢ ( ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) |
16 |
1 2
|
hsmexlem2 |
⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) ) |
17 |
13 14 15 16
|
syl3anc |
⊢ ( ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) ) |
18 |
9 17
|
sseldd |
⊢ ( ( ( 𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On ) ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) ) |