Step | Hyp | Ref
| Expression |
1 | | madeval 31935 |
. 2
⊢ (𝐴 ∈ On → ( M
‘𝐴) = ( |s “
(𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)))) |
2 | | scutcut 31912 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 → ((𝑎 |s 𝑏) ∈ No
∧ 𝑎 <<s {(𝑎 |s 𝑏)} ∧ {(𝑎 |s 𝑏)} <<s 𝑏)) |
3 | 2 | simp1d 1073 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) ∈ No
) |
4 | | eleq1 2689 |
. . . . . . . . 9
⊢ ((𝑎 |s 𝑏) = 𝑥 → ((𝑎 |s 𝑏) ∈ No
↔ 𝑥 ∈ No )) |
5 | 4 | biimpd 219 |
. . . . . . . 8
⊢ ((𝑎 |s 𝑏) = 𝑥 → ((𝑎 |s 𝑏) ∈ No
→ 𝑥 ∈ No )) |
6 | 3, 5 | mpan9 486 |
. . . . . . 7
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
7 | 6 | rexlimivw 3029 |
. . . . . 6
⊢
(∃𝑏 ∈
𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
8 | 7 | rexlimivw 3029 |
. . . . 5
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
9 | 8 | pm4.71ri 665 |
. . . 4
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))) |
10 | 9 | abbii 2739 |
. . 3
⊢ {𝑥 ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))} |
11 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (𝑦 ∈ <<s ↔ 〈𝑎, 𝑏〉 ∈ <<s )) |
12 | | breq1 4656 |
. . . . . . 7
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (𝑦 |s 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
13 | 11, 12 | anbi12d 747 |
. . . . . 6
⊢ (𝑦 = 〈𝑎, 𝑏〉 → ((𝑦 ∈ <<s ∧ 𝑦 |s 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥))) |
14 | 13 | rexxp 5264 |
. . . . 5
⊢
(∃𝑦 ∈
(𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
15 | | imaindm 31682 |
. . . . . . . 8
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s )) |
16 | | dmscut 31918 |
. . . . . . . . . 10
⊢ dom |s =
<<s |
17 | 16 | ineq2i 3811 |
. . . . . . . . 9
⊢
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s ) = ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) |
18 | 17 | imaeq2i 5464 |
. . . . . . . 8
⊢ ( |s
“ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s )) = ( |s “
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) |
19 | 15, 18 | eqtri 2644 |
. . . . . . 7
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) |
20 | 19 | eleq2i 2693 |
. . . . . 6
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ 𝑥 ∈ ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ))) |
21 | | vex 3203 |
. . . . . . 7
⊢ 𝑥 ∈ V |
22 | 21 | elima 5471 |
. . . . . 6
⊢ (𝑥 ∈ ( |s “ ((𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) ↔ ∃𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )𝑦 |s 𝑥) |
23 | | elin 3796 |
. . . . . . . . 9
⊢ (𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s )) |
24 | 23 | anbi1i 731 |
. . . . . . . 8
⊢ ((𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ∧ 𝑦 |s 𝑥) ↔ ((𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥)) |
25 | | anass 681 |
. . . . . . . 8
⊢ (((𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ (𝑦 ∈ <<s ∧ 𝑦 |s 𝑥))) |
26 | 24, 25 | bitri 264 |
. . . . . . 7
⊢ ((𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ∧ 𝑦 |s 𝑥) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ (𝑦 ∈ <<s ∧ 𝑦 |s 𝑥))) |
27 | 26 | rexbii2 3039 |
. . . . . 6
⊢
(∃𝑦 ∈
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )𝑦 |s 𝑥 ↔ ∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥)) |
28 | 20, 22, 27 | 3bitri 286 |
. . . . 5
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ ∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥)) |
29 | | df-br 4654 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
30 | 29 | anbi1i 731 |
. . . . . . 7
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ (𝑎 |s 𝑏) = 𝑥)) |
31 | | df-ov 6653 |
. . . . . . . . . 10
⊢ (𝑎 |s 𝑏) = ( |s ‘〈𝑎, 𝑏〉) |
32 | 31 | eqeq1i 2627 |
. . . . . . . . 9
⊢ ((𝑎 |s 𝑏) = 𝑥 ↔ ( |s ‘〈𝑎, 𝑏〉) = 𝑥) |
33 | | scutf 31919 |
. . . . . . . . . . 11
⊢ |s :
<<s ⟶ No |
34 | | ffn 6045 |
. . . . . . . . . . 11
⊢ ( |s :
<<s ⟶ No → |s Fn <<s
) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . 10
⊢ |s Fn
<<s |
36 | | fnbrfvb 6236 |
. . . . . . . . . 10
⊢ (( |s Fn
<<s ∧ 〈𝑎,
𝑏〉 ∈ <<s )
→ (( |s ‘〈𝑎, 𝑏〉) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
37 | 35, 36 | mpan 706 |
. . . . . . . . 9
⊢
(〈𝑎, 𝑏〉 ∈ <<s →
(( |s ‘〈𝑎, 𝑏〉) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
38 | 32, 37 | syl5bb 272 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ <<s →
((𝑎 |s 𝑏) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
39 | 38 | pm5.32i 669 |
. . . . . . 7
⊢
((〈𝑎, 𝑏〉 ∈ <<s ∧
(𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
40 | 30, 39 | bitri 264 |
. . . . . 6
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
41 | 40 | 2rexbii 3042 |
. . . . 5
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
42 | 14, 28, 41 | 3bitr4i 292 |
. . . 4
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)) |
43 | 42 | abbi2i 2738 |
. . 3
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = {𝑥 ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} |
44 | | df-rab 2921 |
. . 3
⊢ {𝑥 ∈
No ∣ ∃𝑎
∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))} |
45 | 10, 43, 44 | 3eqtr4i 2654 |
. 2
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = {𝑥 ∈ No
∣ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} |
46 | 1, 45 | syl6eq 2672 |
1
⊢ (𝐴 ∈ On → ( M
‘𝐴) = {𝑥 ∈
No ∣ ∃𝑎
∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}) |