Step | Hyp | Ref
| Expression |
1 | | madeval 32899 |
. 2
⊢ (𝐴 ∈ On → ( M
‘𝐴) = ( |s “
(𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)))) |
2 | | scutcut 32876 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 → ((𝑎 |s 𝑏) ∈ No
∧ 𝑎 <<s {(𝑎 |s 𝑏)} ∧ {(𝑎 |s 𝑏)} <<s 𝑏)) |
3 | 2 | simp1d 1135 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) ∈ No
) |
4 | | eleq1 2870 |
. . . . . . . . 9
⊢ ((𝑎 |s 𝑏) = 𝑥 → ((𝑎 |s 𝑏) ∈ No
↔ 𝑥 ∈ No )) |
5 | 4 | biimpd 230 |
. . . . . . . 8
⊢ ((𝑎 |s 𝑏) = 𝑥 → ((𝑎 |s 𝑏) ∈ No
→ 𝑥 ∈ No )) |
6 | 3, 5 | mpan9 507 |
. . . . . . 7
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
7 | 6 | rexlimivw 3245 |
. . . . . 6
⊢
(∃𝑏 ∈
𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
8 | 7 | rexlimivw 3245 |
. . . . 5
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
9 | 8 | pm4.71ri 561 |
. . . 4
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))) |
10 | 9 | abbii 2861 |
. . 3
⊢ {𝑥 ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))} |
11 | | eleq1 2870 |
. . . . . . 7
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (𝑦 ∈ <<s ↔ 〈𝑎, 𝑏〉 ∈ <<s )) |
12 | | breq1 4965 |
. . . . . . 7
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (𝑦 |s 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
13 | 11, 12 | anbi12d 630 |
. . . . . 6
⊢ (𝑦 = 〈𝑎, 𝑏〉 → ((𝑦 ∈ <<s ∧ 𝑦 |s 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥))) |
14 | 13 | rexxp 5599 |
. . . . 5
⊢
(∃𝑦 ∈
(𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
15 | | imaindm 32631 |
. . . . . . . 8
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s )) |
16 | | dmscut 32882 |
. . . . . . . . . 10
⊢ dom |s =
<<s |
17 | 16 | ineq2i 4106 |
. . . . . . . . 9
⊢
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s ) = ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) |
18 | 17 | imaeq2i 5804 |
. . . . . . . 8
⊢ ( |s
“ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s )) = ( |s “
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) |
19 | 15, 18 | eqtri 2819 |
. . . . . . 7
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) |
20 | 19 | eleq2i 2874 |
. . . . . 6
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ 𝑥 ∈ ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ))) |
21 | | vex 3440 |
. . . . . . 7
⊢ 𝑥 ∈ V |
22 | 21 | elima 5811 |
. . . . . 6
⊢ (𝑥 ∈ ( |s “ ((𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) ↔ ∃𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )𝑦 |s 𝑥) |
23 | | elin 4090 |
. . . . . . . . 9
⊢ (𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s )) |
24 | 23 | anbi1i 623 |
. . . . . . . 8
⊢ ((𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ∧ 𝑦 |s 𝑥) ↔ ((𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥)) |
25 | | anass 469 |
. . . . . . . 8
⊢ (((𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ (𝑦 ∈ <<s ∧ 𝑦 |s 𝑥))) |
26 | 24, 25 | bitri 276 |
. . . . . . 7
⊢ ((𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ∧ 𝑦 |s 𝑥) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ (𝑦 ∈ <<s ∧ 𝑦 |s 𝑥))) |
27 | 26 | rexbii2 3209 |
. . . . . 6
⊢
(∃𝑦 ∈
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )𝑦 |s 𝑥 ↔ ∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥)) |
28 | 20, 22, 27 | 3bitri 298 |
. . . . 5
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ ∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥)) |
29 | | df-br 4963 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
30 | 29 | anbi1i 623 |
. . . . . . 7
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ (𝑎 |s 𝑏) = 𝑥)) |
31 | | df-ov 7019 |
. . . . . . . . . 10
⊢ (𝑎 |s 𝑏) = ( |s ‘〈𝑎, 𝑏〉) |
32 | 31 | eqeq1i 2800 |
. . . . . . . . 9
⊢ ((𝑎 |s 𝑏) = 𝑥 ↔ ( |s ‘〈𝑎, 𝑏〉) = 𝑥) |
33 | | scutf 32883 |
. . . . . . . . . . 11
⊢ |s :
<<s ⟶ No |
34 | | ffn 6382 |
. . . . . . . . . . 11
⊢ ( |s :
<<s ⟶ No → |s Fn <<s
) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . 10
⊢ |s Fn
<<s |
36 | | fnbrfvb 6586 |
. . . . . . . . . 10
⊢ (( |s Fn
<<s ∧ 〈𝑎,
𝑏〉 ∈ <<s )
→ (( |s ‘〈𝑎, 𝑏〉) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
37 | 35, 36 | mpan 686 |
. . . . . . . . 9
⊢
(〈𝑎, 𝑏〉 ∈ <<s →
(( |s ‘〈𝑎, 𝑏〉) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
38 | 32, 37 | syl5bb 284 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ <<s →
((𝑎 |s 𝑏) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
39 | 38 | pm5.32i 575 |
. . . . . . 7
⊢
((〈𝑎, 𝑏〉 ∈ <<s ∧
(𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
40 | 30, 39 | bitri 276 |
. . . . . 6
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
41 | 40 | 2rexbii 3212 |
. . . . 5
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
42 | 14, 28, 41 | 3bitr4i 304 |
. . . 4
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)) |
43 | 42 | abbi2i 2922 |
. . 3
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = {𝑥 ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} |
44 | | df-rab 3114 |
. . 3
⊢ {𝑥 ∈
No ∣ ∃𝑎
∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))} |
45 | 10, 43, 44 | 3eqtr4i 2829 |
. 2
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = {𝑥 ∈ No
∣ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} |
46 | 1, 45 | syl6eq 2847 |
1
⊢ (𝐴 ∈ On → ( M
‘𝐴) = {𝑥 ∈
No ∣ ∃𝑎
∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}) |