| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} | 
| 2 | 1 | lrrecfr 27977 | . 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} Fr  No | 
| 3 | 1 | lrrecpo 27975 | . 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} Po  No | 
| 4 | 1 | lrrecse 27976 | . 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} Se  No | 
| 5 |  | no3inds.1 | . 2
⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) | 
| 6 |  | no3inds.2 | . 2
⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) | 
| 7 |  | no3inds.3 | . 2
⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) | 
| 8 |  | no3inds.4 | . 2
⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) | 
| 9 |  | no3inds.5 | . 2
⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) | 
| 10 |  | no3inds.6 | . 2
⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) | 
| 11 |  | no3inds.7 | . 2
⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) | 
| 12 |  | no3inds.8 | . 2
⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) | 
| 13 |  | no3inds.9 | . 2
⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) | 
| 14 |  | no3inds.10 | . 2
⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) | 
| 15 | 1 | lrrecpred 27978 | . . . . . . 7
⊢ (𝑎 ∈ 
No  → Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑎) = (( L ‘𝑎) ∪ ( R ‘𝑎))) | 
| 16 | 15 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑎) = (( L
‘𝑎) ∪ ( R
‘𝑎))) | 
| 17 | 1 | lrrecpred 27978 | . . . . . . . 8
⊢ (𝑏 ∈ 
No  → Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑏) = (( L ‘𝑏) ∪ ( R ‘𝑏))) | 
| 18 | 17 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑏) = (( L
‘𝑏) ∪ ( R
‘𝑏))) | 
| 19 | 1 | lrrecpred 27978 | . . . . . . . . 9
⊢ (𝑐 ∈ 
No  → Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑐) = (( L ‘𝑐) ∪ ( R ‘𝑐))) | 
| 20 | 19 | 3ad2ant3 1135 | . . . . . . . 8
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ Pred({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑐) = (( L
‘𝑐) ∪ ( R
‘𝑐))) | 
| 21 | 20 | raleqdv 3325 | . . . . . . 7
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑓 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑐)𝜃 ↔ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃)) | 
| 22 | 18, 21 | raleqbidv 3345 | . . . . . 6
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑒 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑐)𝜃 ↔ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃)) | 
| 23 | 16, 22 | raleqbidv 3345 | . . . . 5
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑐)𝜃 ↔ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃)) | 
| 24 | 18 | raleqdv 3325 | . . . . . 6
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑒 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑏)𝜒 ↔ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒)) | 
| 25 | 16, 24 | raleqbidv 3345 | . . . . 5
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑎)∀𝑒 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑏)𝜒 ↔ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒)) | 
| 26 | 20 | raleqdv 3325 | . . . . . 6
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑓 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑐)𝜁 ↔ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁)) | 
| 27 | 16, 26 | raleqbidv 3345 | . . . . 5
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑎)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑐)𝜁 ↔ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁)) | 
| 28 | 23, 25, 27 | 3anbi123d 1437 | . . . 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 ‘𝑐))𝜁))) | 
| 29 | 16 | raleqdv 3325 | . . . . 5
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑑 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑎)𝜓 ↔ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))𝜓)) | 
| 30 | 20 | raleqdv 3325 | . . . . . 6
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑓 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑐)𝜏 ↔ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏)) | 
| 31 | 18, 30 | raleqbidv 3345 | . . . . 5
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑒 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑏)∀𝑓 ∈ Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No , 𝑐)𝜏 ↔ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏)) | 
| 32 | 18 | raleqdv 3325 | . . . . 5
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑒 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑏)𝜎 ↔ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜎)) | 
| 33 | 29, 31, 32 | 3anbi123d 1437 | . . . 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 ‘𝑏))𝜎))) | 
| 34 | 20 | raleqdv 3325 | . . . 4
⊢ ((𝑎 ∈ 
No  ∧ 𝑏 ∈
 No  ∧ 𝑐 ∈  No )
→ (∀𝑓 ∈
Pred ({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))},  No
, 𝑐)𝜂 ↔ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜂)) | 
| 35 | 28, 33, 34 | 3anbi123d 1437 | . . 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 ‘𝑐))𝜂))) | 
| 36 |  | 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 ‘𝑐))𝜂) → 𝜑)) | 
| 37 | 35, 36 | sylbid 240 | . 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 , 𝑐)𝜂) → 𝜑)) | 
| 38 | 2, 3, 4, 2, 3, 4, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 37 | xpord3ind 8182 | 1
⊢ ((𝑋 ∈ 
No  ∧ 𝑌 ∈
 No  ∧ 𝑍 ∈  No )
→ 𝜆) |