Step | Hyp | Ref
| Expression |
1 | | df-ov 7175 |
. . 3
⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩) |
2 | | opelxp 5561 |
. . . 4
⊢
(⟨𝐴, 𝐵⟩ ∈ ( No × No ) ↔
(𝐴 ∈ No ∧ 𝐵 ∈ No
)) |
3 | | eqid 2738 |
. . . . . . 7
⊢
{⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} = {⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} |
4 | | eqid 2738 |
. . . . . . 7
⊢
{⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} |
5 | 3, 4 | noxpordfr 33753 |
. . . . . 6
⊢
{⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Fr ( No
× No ) |
6 | 3, 4 | noxpordpo 33752 |
. . . . . 6
⊢
{⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Po ( No
× No ) |
7 | 3, 4 | noxpordse 33754 |
. . . . . 6
⊢
{⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Se ( No
× No ) |
8 | 5, 6, 7 | 3pm3.2i 1340 |
. . . . 5
⊢
({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Fr ( No
× No ) ∧ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Po ( No
× No ) ∧ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Se ( No
× No )) |
9 | | norec2.1 |
. . . . . . 7
⊢ 𝐹 = norec2 (𝐺) |
10 | | df-norec2 33751 |
. . . . . . 7
⊢ norec2
(𝐺) = frecs({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), 𝐺) |
11 | 9, 10 | eqtri 2761 |
. . . . . 6
⊢ 𝐹 = frecs({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), 𝐺) |
12 | 11 | fpr2 33462 |
. . . . 5
⊢
((({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (
No × No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Fr ( No
× No ) ∧ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Po ( No
× No ) ∧ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Se ( No
× No )) ∧ ⟨𝐴, 𝐵⟩ ∈ ( No
× No )) → (𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), ⟨𝐴, 𝐵⟩)))) |
13 | 8, 12 | mpan 690 |
. . . 4
⊢
(⟨𝐴, 𝐵⟩ ∈ ( No × No ) →
(𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), ⟨𝐴, 𝐵⟩)))) |
14 | 2, 13 | sylbir 238 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), ⟨𝐴, 𝐵⟩)))) |
15 | 1, 14 | syl5eq 2785 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), ⟨𝐴, 𝐵⟩)))) |
16 | 3, 4 | noxpordpred 33755 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), ⟨𝐴, 𝐵⟩) = ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩})) |
17 | 16 | reseq2d 5825 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), ⟨𝐴, 𝐵⟩)) = (𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩}))) |
18 | 17 | oveq2d 7188 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No
× No ) ∧ 𝑏 ∈ ( No
× No ) ∧ (((1^{st} ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^{st} ‘𝑏) ∨ (1^{st} ‘𝑎) = (1^{st} ‘𝑏)) ∧ ((2^{nd}
‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^{nd} ‘𝑏) ∨ (2^{nd} ‘𝑎) = (2^{nd} ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No
× No ), ⟨𝐴, 𝐵⟩))) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩})))) |
19 | 15, 18 | eqtrd 2773 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩})))) |