Proof of Theorem on2recsov
| Step | Hyp | Ref
| Expression |
| 1 | | df-ov 7434 |
. . 3
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
| 2 | | opelxp 5721 |
. . . 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 6423 |
. . . . . . . . 9
⊢ E Fr
On |
| 5 | 4 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ E Fr On) |
| 6 | 3, 5, 5 | frxp2 8169 |
. . . . . . 7
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On ×
On)) |
| 7 | 6 | mptru 1547 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On ×
On) |
| 8 | | epweon 7795 |
. . . . . . . . . 10
⊢ E We
On |
| 9 | | weso 5676 |
. . . . . . . . . 10
⊢ ( E We On
→ E Or On) |
| 10 | | sopo 5611 |
. . . . . . . . . 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 8168 |
. . . . . . 7
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On ×
On)) |
| 14 | 13 | mptru 1547 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On ×
On) |
| 15 | | epse 5667 |
. . . . . . . . 9
⊢ E Se
On |
| 16 | 15 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ E Se On) |
| 17 | 3, 16, 16 | sexp2 8171 |
. . . . . . 7
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On ×
On)) |
| 18 | 17 | mptru 1547 |
. . . . . 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 8329 |
. . . . 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 690 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ∈ (On × On)
→ (𝐹‘〈𝐴, 𝐵〉) = (〈𝐴, 𝐵〉𝐺(𝐹 ↾ Pred({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 〈𝐴, 𝐵〉)))) |
| 23 | 2, 22 | sylbir 235 |
. . 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 8170 |
. . . . 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 7806 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → Pred( E , On,
𝐴) = 𝐴) |
| 27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Pred( E , On,
𝐴) = 𝐴) |
| 28 | 27 | uneq1d 4167 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐴) ∪ {𝐴}) = (𝐴 ∪ {𝐴})) |
| 29 | | df-suc 6390 |
. . . . . . . 8
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
| 30 | 28, 29 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐴) ∪ {𝐴}) = suc 𝐴) |
| 31 | | predon 7806 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → Pred( E , On,
𝐵) = 𝐵) |
| 32 | 31 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Pred( E , On,
𝐵) = 𝐵) |
| 33 | 32 | uneq1d 4167 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐵) ∪ {𝐵}) = (𝐵 ∪ {𝐵})) |
| 34 | | df-suc 6390 |
. . . . . . . 8
⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) |
| 35 | 33, 34 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐵) ∪ {𝐵}) = suc 𝐵) |
| 36 | 30, 35 | xpeq12d 5716 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((Pred( E ,
On, 𝐴) ∪ {𝐴}) × (Pred( E , On, 𝐵) ∪ {𝐵})) = (suc 𝐴 × suc 𝐵)) |
| 37 | 36 | difeq1d 4125 |
. . . . 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 5997 |
. . 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 7447 |
. 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 𝐵) ∖ {〈𝐴, 𝐵〉})))) |