| Step | Hyp | Ref
| Expression |
| 1 | | madeval 27891 |
. 2
⊢ (𝐴 ∈ On → ( M
‘𝐴) = ( |s “
(𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)))) |
| 2 | | scutcl 27847 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) ∈ No
) |
| 3 | | eleq1 2829 |
. . . . . . . . 9
⊢ ((𝑎 |s 𝑏) = 𝑥 → ((𝑎 |s 𝑏) ∈ No
↔ 𝑥 ∈ No )) |
| 4 | 3 | biimpd 229 |
. . . . . . . 8
⊢ ((𝑎 |s 𝑏) = 𝑥 → ((𝑎 |s 𝑏) ∈ No
→ 𝑥 ∈ No )) |
| 5 | 2, 4 | mpan9 506 |
. . . . . . 7
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
| 6 | 5 | rexlimivw 3151 |
. . . . . 6
⊢
(∃𝑏 ∈
𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
| 7 | 6 | rexlimivw 3151 |
. . . . 5
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No
) |
| 8 | 7 | pm4.71ri 560 |
. . . 4
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))) |
| 9 | 8 | abbii 2809 |
. . 3
⊢ {𝑥 ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))} |
| 10 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (𝑦 ∈ <<s ↔ 〈𝑎, 𝑏〉 ∈ <<s )) |
| 11 | | breq1 5146 |
. . . . . . 7
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (𝑦 |s 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
| 12 | 10, 11 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = 〈𝑎, 𝑏〉 → ((𝑦 ∈ <<s ∧ 𝑦 |s 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥))) |
| 13 | 12 | rexxp 5853 |
. . . . 5
⊢
(∃𝑦 ∈
(𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
| 14 | | imaindm 6319 |
. . . . . . . 8
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s )) |
| 15 | | dmscut 27856 |
. . . . . . . . . 10
⊢ dom |s =
<<s |
| 16 | 15 | ineq2i 4217 |
. . . . . . . . 9
⊢
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s ) = ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) |
| 17 | 16 | imaeq2i 6076 |
. . . . . . . 8
⊢ ( |s
“ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s )) = ( |s “
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) |
| 18 | 14, 17 | eqtri 2765 |
. . . . . . 7
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) |
| 19 | 18 | eleq2i 2833 |
. . . . . 6
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ 𝑥 ∈ ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ))) |
| 20 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 21 | 20 | elima 6083 |
. . . . . 6
⊢ (𝑥 ∈ ( |s “ ((𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) ↔ ∃𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )𝑦 |s 𝑥) |
| 22 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s )) |
| 23 | 22 | anbi1i 624 |
. . . . . . . 8
⊢ ((𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ∧ 𝑦 |s 𝑥) ↔ ((𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥)) |
| 24 | | anass 468 |
. . . . . . . 8
⊢ (((𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ (𝑦 ∈ <<s ∧ 𝑦 |s 𝑥))) |
| 25 | 23, 24 | bitri 275 |
. . . . . . 7
⊢ ((𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ∧ 𝑦 |s 𝑥) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ (𝑦 ∈ <<s ∧ 𝑦 |s 𝑥))) |
| 26 | 25 | rexbii2 3090 |
. . . . . 6
⊢
(∃𝑦 ∈
((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )𝑦 |s 𝑥 ↔ ∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥)) |
| 27 | 19, 21, 26 | 3bitri 297 |
. . . . 5
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ ∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥)) |
| 28 | | df-br 5144 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
| 29 | 28 | anbi1i 624 |
. . . . . . 7
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ (𝑎 |s 𝑏) = 𝑥)) |
| 30 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑎 |s 𝑏) = ( |s ‘〈𝑎, 𝑏〉) |
| 31 | 30 | eqeq1i 2742 |
. . . . . . . . 9
⊢ ((𝑎 |s 𝑏) = 𝑥 ↔ ( |s ‘〈𝑎, 𝑏〉) = 𝑥) |
| 32 | | scutf 27857 |
. . . . . . . . . . 11
⊢ |s :
<<s ⟶ No |
| 33 | | ffn 6736 |
. . . . . . . . . . 11
⊢ ( |s :
<<s ⟶ No → |s Fn <<s
) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . . . 10
⊢ |s Fn
<<s |
| 35 | | fnbrfvb 6959 |
. . . . . . . . . 10
⊢ (( |s Fn
<<s ∧ 〈𝑎,
𝑏〉 ∈ <<s )
→ (( |s ‘〈𝑎, 𝑏〉) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
| 36 | 34, 35 | mpan 690 |
. . . . . . . . 9
⊢
(〈𝑎, 𝑏〉 ∈ <<s →
(( |s ‘〈𝑎, 𝑏〉) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
| 37 | 31, 36 | bitrid 283 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ <<s →
((𝑎 |s 𝑏) = 𝑥 ↔ 〈𝑎, 𝑏〉 |s 𝑥)) |
| 38 | 37 | pm5.32i 574 |
. . . . . . 7
⊢
((〈𝑎, 𝑏〉 ∈ <<s ∧
(𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
| 39 | 29, 38 | bitri 275 |
. . . . . 6
⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
| 40 | 39 | 2rexbii 3129 |
. . . . 5
⊢
(∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(〈𝑎, 𝑏〉 ∈ <<s ∧ 〈𝑎, 𝑏〉 |s 𝑥)) |
| 41 | 13, 27, 40 | 3bitr4i 303 |
. . . 4
⊢ (𝑥 ∈ ( |s “ (𝒫
∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)) |
| 42 | 41 | eqabi 2877 |
. . 3
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = {𝑥 ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} |
| 43 | | df-rab 3437 |
. . 3
⊢ {𝑥 ∈
No ∣ ∃𝑎
∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ No
∧ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))} |
| 44 | 9, 42, 43 | 3eqtr4i 2775 |
. 2
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = {𝑥 ∈ No
∣ ∃𝑎 ∈
𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} |
| 45 | 1, 44 | eqtrdi 2793 |
1
⊢ (𝐴 ∈ On → ( M
‘𝐴) = {𝑥 ∈
No ∣ ∃𝑎
∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}) |