Step | Hyp | Ref
| Expression |
1 | | df-ov 7365 |
. . 3
⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩) |
2 | | opelxp 5674 |
. . . 4
⊢
(⟨𝐴, 𝐵⟩ ∈ (On × On)
↔ (𝐴 ∈ On ∧
𝐵 ∈
On)) |
3 | | eqid 2737 |
. . . . . . . 8
⊢
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))} |
4 | | onfr 6361 |
. . . . . . . . 9
⊢ E Fr
On |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ E Fr On) |
6 | 3, 5, 5 | frxp2 8081 |
. . . . . . 7
⊢ (⊤
→ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On ×
On)) |
7 | 6 | mptru 1549 |
. . . . . 6
⊢
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On ×
On) |
8 | | epweon 7714 |
. . . . . . . . . 10
⊢ E We
On |
9 | | weso 5629 |
. . . . . . . . . 10
⊢ ( E We On
→ E Or On) |
10 | | sopo 5569 |
. . . . . . . . . 10
⊢ ( E Or On
→ E Po On) |
11 | 8, 9, 10 | mp2b 10 |
. . . . . . . . 9
⊢ E Po
On |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ E Po On) |
13 | 3, 12, 12 | poxp2 8080 |
. . . . . . 7
⊢ (⊤
→ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On ×
On)) |
14 | 13 | mptru 1549 |
. . . . . 6
⊢
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On ×
On) |
15 | | epse 5621 |
. . . . . . . . 9
⊢ E Se
On |
16 | 15 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ E Se On) |
17 | 3, 16, 16 | sexp2 8083 |
. . . . . . 7
⊢ (⊤
→ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On ×
On)) |
18 | 17 | mptru 1549 |
. . . . . 6
⊢
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On ×
On) |
19 | 7, 14, 18 | 3pm3.2i 1340 |
. . . . 5
⊢
({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On × On) ∧
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On × On) ∧
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On ×
On)) |
20 | | on2recs.1 |
. . . . . 6
⊢ 𝐹 = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 𝐺) |
21 | 20 | fpr2 8240 |
. . . . 5
⊢
((({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On × On) ∧
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On × On) ∧
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On × On)) ∧
⟨𝐴, 𝐵⟩ ∈ (On × On)) → (𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), ⟨𝐴, 𝐵⟩)))) |
22 | 19, 21 | mpan 689 |
. . . 4
⊢
(⟨𝐴, 𝐵⟩ ∈ (On × On)
→ (𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), ⟨𝐴, 𝐵⟩)))) |
23 | 2, 22 | sylbir 234 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), ⟨𝐴, 𝐵⟩)))) |
24 | 1, 23 | eqtrid 2789 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), ⟨𝐴, 𝐵⟩)))) |
25 | 3 | xpord2pred 8082 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
Pred({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))}, (On × On),
⟨𝐴, 𝐵⟩) = (((Pred( E , On, 𝐴) ∪ {𝐴}) × (Pred( E , On, 𝐵) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩})) |
26 | | predon 7725 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → Pred( E , On,
𝐴) = 𝐴) |
27 | 26 | adantr 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Pred( E , On,
𝐴) = 𝐴) |
28 | 27 | uneq1d 4127 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐴) ∪ {𝐴}) = (𝐴 ∪ {𝐴})) |
29 | | df-suc 6328 |
. . . . . . . 8
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
30 | 28, 29 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐴) ∪ {𝐴}) = suc 𝐴) |
31 | | predon 7725 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → Pred( E , On,
𝐵) = 𝐵) |
32 | 31 | adantl 483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Pred( E , On,
𝐵) = 𝐵) |
33 | 32 | uneq1d 4127 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐵) ∪ {𝐵}) = (𝐵 ∪ {𝐵})) |
34 | | df-suc 6328 |
. . . . . . . 8
⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) |
35 | 33, 34 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐵) ∪ {𝐵}) = suc 𝐵) |
36 | 30, 35 | xpeq12d 5669 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((Pred( E ,
On, 𝐴) ∪ {𝐴}) × (Pred( E , On, 𝐵) ∪ {𝐵})) = (suc 𝐴 × suc 𝐵)) |
37 | 36 | difeq1d 4086 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((Pred( E ,
On, 𝐴) ∪ {𝐴}) × (Pred( E , On, 𝐵) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩}) = ((suc 𝐴 × suc 𝐵) ∖ {⟨𝐴, 𝐵⟩})) |
38 | 25, 37 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
Pred({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))}, (On × On),
⟨𝐴, 𝐵⟩) = ((suc 𝐴 × suc 𝐵) ∖ {⟨𝐴, 𝐵⟩})) |
39 | 38 | reseq2d 5942 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹 ↾ Pred({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), ⟨𝐴, 𝐵⟩)) = (𝐹 ↾ ((suc 𝐴 × suc 𝐵) ∖ {⟨𝐴, 𝐵⟩}))) |
40 | 39 | oveq2d 7378 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), ⟨𝐴, 𝐵⟩))) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((suc 𝐴 × suc 𝐵) ∖ {⟨𝐴, 𝐵⟩})))) |
41 | 24, 40 | eqtrd 2777 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((suc 𝐴 × suc 𝐵) ∖ {⟨𝐴, 𝐵⟩})))) |