Step |
Hyp |
Ref |
Expression |
1 |
|
frege130.m |
⊢ 𝑀 ∈ 𝑈 |
2 |
|
frege130.r |
⊢ 𝑅 ∈ 𝑉 |
3 |
|
vex |
⊢ 𝑎 ∈ V |
4 |
|
vex |
⊢ 𝑏 ∈ V |
5 |
3 4 1 2
|
frege129 |
⊢ ( Fun ◡ ◡ 𝑅 → ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) ) |
6 |
5
|
alrimdv |
⊢ ( Fun ◡ ◡ 𝑅 → ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) ) |
7 |
6
|
alrimiv |
⊢ ( Fun ◡ ◡ 𝑅 → ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) ) |
8 |
|
frege9 |
⊢ ( ( Fun ◡ ◡ 𝑅 → ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) ) → ( ( ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) → ( Fun ◡ ◡ 𝑅 → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) ) |
9 |
7 8
|
ax-mp |
⊢ ( ( ∀ 𝑏 ( ( ¬ 𝑏 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑏 ) → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → ( ¬ 𝑎 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) ) ) → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) → ( Fun ◡ ◡ 𝑅 → 𝑅 hereditary ( ( ◡ ( t+ ‘ 𝑅 ) “ { 𝑀 } ) ∪ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑀 } ) ) ) ) |