Proof of Theorem on2recsov
Step | Hyp | Ref
| Expression |
1 | | df-ov 7221 |
. . 3
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
2 | | opelxp 5592 |
. . . 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 6257 |
. . . . . . . . 9
⊢ E Fr
On |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ E Fr On) |
6 | 3, 5, 5 | frxp2 33533 |
. . . . . . 7
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On ×
On)) |
7 | 6 | mptru 1550 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On ×
On) |
8 | | epweon 7565 |
. . . . . . . . . 10
⊢ E We
On |
9 | | weso 5547 |
. . . . . . . . . 10
⊢ ( E We On
→ E Or On) |
10 | | sopo 5492 |
. . . . . . . . . 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 33532 |
. . . . . . 7
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On ×
On)) |
14 | 13 | mptru 1550 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On ×
On) |
15 | | epse 5539 |
. . . . . . . . 9
⊢ E Se
On |
16 | 15 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ E Se On) |
17 | 3, 16, 16 | sexp2 33535 |
. . . . . . 7
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On ×
On)) |
18 | 17 | mptru 1550 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On ×
On) |
19 | 7, 14, 18 | 3pm3.2i 1341 |
. . . . 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 8049 |
. . . . 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 238 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐹‘〈𝐴, 𝐵〉) = (〈𝐴, 𝐵〉𝐺(𝐹 ↾ Pred({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 〈𝐴, 𝐵〉)))) |
24 | 1, 23 | syl5eq 2790 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐹𝐵) = (〈𝐴, 𝐵〉𝐺(𝐹 ↾ Pred({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 〈𝐴, 𝐵〉)))) |
25 | 3 | xpord2pred 33534 |
. . . . 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 7574 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → Pred( E , On,
𝐴) = 𝐴) |
27 | 26 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Pred( E , On,
𝐴) = 𝐴) |
28 | 27 | uneq1d 4081 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐴) ∪ {𝐴}) = (𝐴 ∪ {𝐴})) |
29 | | df-suc 6224 |
. . . . . . . 8
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
30 | 28, 29 | eqtr4di 2796 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐴) ∪ {𝐴}) = suc 𝐴) |
31 | | predon 7574 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → Pred( E , On,
𝐵) = 𝐵) |
32 | 31 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Pred( E , On,
𝐵) = 𝐵) |
33 | 32 | uneq1d 4081 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐵) ∪ {𝐵}) = (𝐵 ∪ {𝐵})) |
34 | | df-suc 6224 |
. . . . . . . 8
⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) |
35 | 33, 34 | eqtr4di 2796 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Pred( E ,
On, 𝐵) ∪ {𝐵}) = suc 𝐵) |
36 | 30, 35 | xpeq12d 5587 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((Pred( E ,
On, 𝐴) ∪ {𝐴}) × (Pred( E , On, 𝐵) ∪ {𝐵})) = (suc 𝐴 × suc 𝐵)) |
37 | 36 | difeq1d 4041 |
. . . . 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 5856 |
. . 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 7234 |
. 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 𝐵) ∖ {〈𝐴, 𝐵〉})))) |