Step | Hyp | Ref
| Expression |
1 | | imass2 5942 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝐵 → ( M “ 𝐴) ⊆ ( M “ 𝐵)) |
2 | 1 | 3ad2ant3 1132 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → ( M “ 𝐴) ⊆ ( M “ 𝐵)) |
3 | 2 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ No )
→ ( M “ 𝐴)
⊆ ( M “ 𝐵)) |
4 | 3 | unissd 4811 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ No )
→ ∪ ( M “ 𝐴) ⊆ ∪ ( M
“ 𝐵)) |
5 | 4 | sspwd 4512 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ No )
→ 𝒫 ∪ ( M “ 𝐴) ⊆ 𝒫 ∪ ( M “ 𝐵)) |
6 | | ssrexv 3961 |
. . . . . 6
⊢
(𝒫 ∪ ( M “ 𝐴) ⊆ 𝒫 ∪ ( M “ 𝐵) → (∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ No )
→ (∃𝑙 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) |
8 | | ssrexv 3961 |
. . . . . . 7
⊢
(𝒫 ∪ ( M “ 𝐴) ⊆ 𝒫 ∪ ( M “ 𝐵) → (∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) |
9 | 5, 8 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ No )
→ (∃𝑟 ∈
𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) |
10 | 9 | reximdv 3197 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ No )
→ (∃𝑙 ∈
𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) |
11 | 7, 10 | syld 47 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ No )
→ (∃𝑙 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) |
12 | 11 | ralrimiva 3113 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → ∀𝑥 ∈ No
(∃𝑙 ∈ 𝒫
∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) |
13 | | ss2rab 3977 |
. . 3
⊢ ({𝑥 ∈
No ∣ ∃𝑙
∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} ⊆ {𝑥 ∈ No
∣ ∃𝑙 ∈
𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} ↔ ∀𝑥 ∈ No
(∃𝑙 ∈ 𝒫
∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) |
14 | 12, 13 | sylibr 237 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → {𝑥 ∈ No
∣ ∃𝑙 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} ⊆ {𝑥 ∈ No
∣ ∃𝑙 ∈
𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)}) |
15 | | madeval2 33631 |
. . 3
⊢ (𝐴 ∈ On → ( M
‘𝐴) = {𝑥 ∈
No ∣ ∃𝑙
∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)}) |
16 | 15 | 3ad2ant1 1130 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → ( M ‘𝐴) = {𝑥 ∈ No
∣ ∃𝑙 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)}) |
17 | | madeval2 33631 |
. . 3
⊢ (𝐵 ∈ On → ( M
‘𝐵) = {𝑥 ∈
No ∣ ∃𝑙
∈ 𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)}) |
18 | 17 | 3ad2ant2 1131 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → ( M ‘𝐵) = {𝑥 ∈ No
∣ ∃𝑙 ∈
𝒫 ∪ ( M “ 𝐵)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐵)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)}) |
19 | 14, 16, 18 | 3sstr4d 3941 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → ( M ‘𝐴) ⊆ ( M ‘𝐵)) |