Step |
Hyp |
Ref |
Expression |
1 |
|
frpoinsg.1 |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) ) |
2 |
|
dfss3 |
⊢ ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) 𝑧 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) |
3 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐴 |
4 |
3
|
elrabsf |
⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑦 ] 𝜑 ) ) |
5 |
4
|
simprbi |
⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → [ 𝑧 / 𝑦 ] 𝜑 ) |
6 |
5
|
ralimi |
⊢ ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) 𝑧 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 ) |
7 |
2 6
|
sylbi |
⊢ ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 ) |
8 |
|
nfv |
⊢ Ⅎ 𝑦 ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) |
9 |
|
nfcv |
⊢ Ⅎ 𝑦 Pred ( 𝑅 , 𝐴 , 𝑤 ) |
10 |
|
nfsbc1v |
⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜑 |
11 |
9 10
|
nfralw |
⊢ Ⅎ 𝑦 ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 |
12 |
|
nfsbc1v |
⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜑 |
13 |
11 12
|
nfim |
⊢ Ⅎ 𝑦 ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) |
14 |
8 13
|
nfim |
⊢ Ⅎ 𝑦 ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) ) |
15 |
|
eleq1w |
⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) ) |
16 |
15
|
anbi2d |
⊢ ( 𝑦 = 𝑤 → ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ↔ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ) ) |
17 |
|
predeq3 |
⊢ ( 𝑦 = 𝑤 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑤 ) ) |
18 |
17
|
raleqdv |
⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 ) ) |
19 |
|
sbceq1a |
⊢ ( 𝑦 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑦 ] 𝜑 ) ) |
20 |
18 19
|
imbi12d |
⊢ ( 𝑦 = 𝑤 → ( ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) ↔ ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) ) ) |
21 |
16 20
|
imbi12d |
⊢ ( 𝑦 = 𝑤 → ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) [ 𝑧 / 𝑦 ] 𝜑 → 𝜑 ) ) ↔ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) ) ) ) |
22 |
14 21 1
|
chvarfv |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑤 ) [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) ) |
23 |
7 22
|
syl5 |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → [ 𝑤 / 𝑦 ] 𝜑 ) ) |
24 |
|
simpr |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ 𝐴 ) |
25 |
23 24
|
jctild |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑦 ] 𝜑 ) ) ) |
26 |
3
|
elrabsf |
⊢ ( 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑦 ] 𝜑 ) ) |
27 |
25 26
|
syl6ibr |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) ) |
28 |
27
|
ralrimiva |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑤 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) ) |
29 |
|
ssrab2 |
⊢ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 |
30 |
28 29
|
jctil |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) ) ) |
31 |
|
frpoind |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ { 𝑦 ∈ 𝐴 ∣ 𝜑 } → 𝑤 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) ) ) → 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) |
32 |
30 31
|
mpdan |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) |
33 |
|
rabid2 |
⊢ ( 𝐴 = { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝐴 𝜑 ) |
34 |
32 33
|
sylib |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 ) |