Step |
Hyp |
Ref |
Expression |
1 |
|
noinds.1 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
noinds.2 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) ) |
3 |
|
noinds.3 |
⊢ ( 𝑥 ∈ No → ( ∀ 𝑦 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 → 𝜑 ) ) |
4 |
|
eqid |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } = { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } |
5 |
4
|
lrrecfr |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Fr No |
6 |
4
|
lrrecpo |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Po No |
7 |
4
|
lrrecse |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Se No |
8 |
5 6 7
|
3pm3.2i |
⊢ ( { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Fr No ∧ { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Po No ∧ { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Se No ) |
9 |
4
|
lrrecpred |
⊢ ( 𝑥 ∈ No → Pred ( { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } , No , 𝑥 ) = ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) |
10 |
9
|
raleqdv |
⊢ ( 𝑥 ∈ No → ( ∀ 𝑦 ∈ Pred ( { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } , No , 𝑥 ) 𝜓 ↔ ∀ 𝑦 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜓 ) ) |
11 |
10 3
|
sylbid |
⊢ ( 𝑥 ∈ No → ( ∀ 𝑦 ∈ Pred ( { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } , No , 𝑥 ) 𝜓 → 𝜑 ) ) |
12 |
11 1 2
|
frpoins3g |
⊢ ( ( ( { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Fr No ∧ { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Po No ∧ { 〈 𝑎 , 𝑏 〉 ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } Se No ) ∧ 𝐴 ∈ No ) → 𝜒 ) |
13 |
8 12
|
mpan |
⊢ ( 𝐴 ∈ No → 𝜒 ) |