Description: The transitive predecessors under a relation form a set.
This is the first theorem in the transitive predecessor series that requires the axiom of infinity. (Contributed by Scott Fenton, 18-Feb-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | trpredex | ⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-trpred | ⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) | |
2 | frfnom | ⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω | |
3 | omex | ⊢ ω ∈ V | |
4 | fnex | ⊢ ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω ∧ ω ∈ V ) → ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ∈ V ) | |
5 | 2 3 4 | mp2an | ⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ∈ V |
6 | 5 | rnex | ⊢ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ∈ V |
7 | 6 | uniex | ⊢ ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ∈ V |
8 | 1 7 | eqeltri | ⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V |