Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. 2
⊢
{〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((
No × No ) × No ) ∧ 𝑤 ∈ (( No
× No ) × No
) ∧ ((((1st ‘(1st ‘𝑧)){〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} (1st ‘(1st
‘𝑤)) ∨
(1st ‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑤))) ∧
((2nd ‘(1st ‘𝑧)){〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} (2nd ‘(1st
‘𝑤)) ∨
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑤))) ∧
((2nd ‘𝑧){〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} (2nd ‘𝑤) ∨ (2nd ‘𝑧) = (2nd ‘𝑤))) ∧ 𝑧 ≠ 𝑤))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (( No
× No ) × No
) ∧ 𝑤 ∈
(( No × No )
× No ) ∧ ((((1st
‘(1st ‘𝑧)){〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} (1st ‘(1st
‘𝑤)) ∨
(1st ‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑤))) ∧
((2nd ‘(1st ‘𝑧)){〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} (2nd ‘(1st
‘𝑤)) ∨
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑤))) ∧
((2nd ‘𝑧){〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} (2nd ‘𝑤) ∨ (2nd ‘𝑧) = (2nd ‘𝑤))) ∧ 𝑧 ≠ 𝑤))} |
2 | | eqid 2739 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} |
3 | 2 | lrrecfr 33870 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} Fr No
|
4 | 2 | lrrecpo 33868 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} Po No
|
5 | 2 | lrrecse 33869 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} Se No
|
6 | | no3inds.1 |
. 2
⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) |
7 | | no3inds.2 |
. 2
⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) |
8 | | no3inds.3 |
. 2
⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) |
9 | | no3inds.4 |
. 2
⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) |
10 | | no3inds.5 |
. 2
⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) |
11 | | no3inds.6 |
. 2
⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) |
12 | | no3inds.7 |
. 2
⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) |
13 | | no3inds.8 |
. 2
⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) |
14 | | no3inds.9 |
. 2
⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) |
15 | | no3inds.10 |
. 2
⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) |
16 | 2 | lrrecpred 33871 |
. . . . . . 7
⊢ (𝑎 ∈
No → Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎) = (( L ‘𝑎) ∪ ( R ‘𝑎))) |
17 | 16 | 3ad2ant1 1135 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎) = (( L
‘𝑎) ∪ ( R
‘𝑎))) |
18 | 2 | lrrecpred 33871 |
. . . . . . . 8
⊢ (𝑏 ∈
No → Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏) = (( L ‘𝑏) ∪ ( R ‘𝑏))) |
19 | 18 | 3ad2ant2 1136 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑏) = (( L
‘𝑏) ∪ ( R
‘𝑏))) |
20 | 2 | lrrecpred 33871 |
. . . . . . . . 9
⊢ (𝑐 ∈
No → Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐) = (( L ‘𝑐) ∪ ( R ‘𝑐))) |
21 | 20 | 3ad2ant3 1137 |
. . . . . . . 8
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑐) = (( L
‘𝑐) ∪ ( R
‘𝑐))) |
22 | 21 | raleqdv 3340 |
. . . . . . 7
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑓 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑐)𝜃 ↔ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃)) |
23 | 19, 22 | raleqbidv 3328 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑒 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜃 ↔ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃)) |
24 | 17, 23 | raleqbidv 3328 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜃 ↔ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃)) |
25 | 19 | raleqdv 3340 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑒 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑏)𝜒 ↔ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒)) |
26 | 17, 25 | raleqbidv 3328 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)𝜒 ↔ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒)) |
27 | 21 | raleqdv 3340 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑓 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑐)𝜁 ↔ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁)) |
28 | 17, 27 | raleqbidv 3328 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜁 ↔ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁)) |
29 | 24, 26, 28 | 3anbi123d 1438 |
. . . 4
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ ((∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜁) ↔ (∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁))) |
30 | 17 | raleqdv 3340 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎)𝜓 ↔ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))𝜓)) |
31 | 21 | raleqdv 3340 |
. . . . . 6
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑓 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑐)𝜏 ↔ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏)) |
32 | 19, 31 | raleqbidv 3328 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑒 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜏 ↔ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏)) |
33 | 19 | raleqdv 3340 |
. . . . 5
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑒 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑏)𝜎 ↔ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜎)) |
34 | 30, 32, 33 | 3anbi123d 1438 |
. . . 4
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ ((∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)𝜎) ↔ (∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))𝜓 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜎))) |
35 | 21 | raleqdv 3340 |
. . . 4
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (∀𝑓 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑐)𝜂 ↔ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜂)) |
36 | 29, 34, 35 | 3anbi123d 1438 |
. . 3
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (((∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜂) ↔ ((∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁) ∧ (∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))𝜓 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜎) ∧ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜂))) |
37 | | no3inds.i |
. . 3
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (((∀𝑑 ∈
(( L ‘𝑎) ∪ ( R
‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁) ∧ (∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))𝜓 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜎) ∧ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜂) → 𝜑)) |
38 | 36, 37 | sylbid 243 |
. 2
⊢ ((𝑎 ∈
No ∧ 𝑏 ∈
No ∧ 𝑐 ∈ No )
→ (((∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝑐)𝜂) → 𝜑)) |
39 | 1, 3, 4, 5, 3, 4, 5, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 38 | xpord3ind 33570 |
1
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ 𝑍 ∈ No )
→ 𝜆) |