Proof of Theorem on2recsfn
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (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
‘𝑦)) ∧ 𝑥 ≠ 𝑦))} | 
| 2 |  | onfr 6423 | . . . . 5
⊢  E Fr
On | 
| 3 | 2 | a1i 11 | . . . 4
⊢ (⊤
→ E Fr On) | 
| 4 | 1, 3, 3 | frxp2 8169 | . . 3
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On ×
On)) | 
| 5 | 4 | mptru 1547 | . 2
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Fr (On ×
On) | 
| 6 |  | epweon 7795 | . . . . . 6
⊢  E We
On | 
| 7 |  | weso 5676 | . . . . . 6
⊢ ( E We On
→ E Or On) | 
| 8 |  | sopo 5611 | . . . . . 6
⊢ ( E Or On
→ E Po On) | 
| 9 | 6, 7, 8 | mp2b 10 | . . . . 5
⊢  E Po
On | 
| 10 | 9 | a1i 11 | . . . 4
⊢ (⊤
→ E Po On) | 
| 11 | 1, 10, 10 | poxp2 8168 | . . 3
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On ×
On)) | 
| 12 | 11 | mptru 1547 | . 2
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Po (On ×
On) | 
| 13 |  | epse 5667 | . . . . 5
⊢  E Se
On | 
| 14 | 13 | a1i 11 | . . . 4
⊢ (⊤
→ E Se On) | 
| 15 | 1, 14, 14 | sexp2 8171 | . . 3
⊢ (⊤
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On ×
On)) | 
| 16 | 15 | mptru 1547 | . 2
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧
𝑦 ∈ (On × On)
∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥) E (2nd
‘𝑦) ∨
(2nd ‘𝑥) =
(2nd ‘𝑦))
∧ 𝑥 ≠ 𝑦))} Se (On ×
On) | 
| 17 |  | on2recs.1 | . . 3
⊢ 𝐹 = frecs({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧
(((1st ‘𝑥)
E (1st ‘𝑦)
∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd
‘𝑥) = (2nd
‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 𝐺) | 
| 18 | 17 | fpr1 8328 | . 2
⊢
(({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (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)) →
𝐹 Fn (On ×
On)) | 
| 19 | 5, 12, 16, 18 | mp3an 1463 | 1
⊢ 𝐹 Fn (On ×
On) |