Metamath Proof Explorer

Theorem trfr

Description: A transitive class well-founded by e. is a subclass of the class of well-founded sets. Part of Lemma I.9.21 of Kunen2 p. 53. (Contributed by Eric Schmidt, 26-Oct-2025)

Ref Expression
Assertion trfr ( ( Tr 𝐴 ∧ E Fr 𝐴 ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )

Proof

Step Hyp Ref Expression
1 epse ⊢ E Se 𝐴
2 r19.21v ⊢ ( ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) ( Tr 𝐴 → 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( Tr 𝐴 → ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) )
3 trpred ⊢ ( ( Tr 𝐴 ∧ 𝑦 ∈ 𝐴 ) → Pred ( E , 𝐴 , 𝑦 ) = 𝑦 )
4 raleq ⊢ ( Pred ( E , 𝐴 , 𝑦 ) = 𝑦 → ( ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) 𝑧 ∈ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑧 ∈ 𝑦 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) )
5 dfss3 ⊢ ( 𝑦 ⊆ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑧 ∈ 𝑦 𝑧 ∈ ∪ ( 𝑅1 “ On ) )
6 4 5 bitr4di ⊢ ( Pred ( E , 𝐴 , 𝑦 ) = 𝑦 → ( ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) 𝑧 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑦 ⊆ ∪ ( 𝑅1 “ On ) ) )
7 vex ⊢ 𝑦 ∈ V
8 7 r1elss ⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑦 ⊆ ∪ ( 𝑅1 “ On ) )
9 6 8 bitr4di ⊢ ( Pred ( E , 𝐴 , 𝑦 ) = 𝑦 → ( ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) 𝑧 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
10 3 9 syl ⊢ ( ( Tr 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) 𝑧 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
11 10 biimpd ⊢ ( ( Tr 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) 𝑧 ∈ ∪ ( 𝑅1 “ On ) → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
12 11 expcom ⊢ ( 𝑦 ∈ 𝐴 → ( Tr 𝐴 → ( ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) 𝑧 ∈ ∪ ( 𝑅1 “ On ) → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) ) )
13 12 a2d ⊢ ( 𝑦 ∈ 𝐴 → ( ( Tr 𝐴 → ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) → ( Tr 𝐴 → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) ) )
14 2 13 biimtrid ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( E , 𝐴 , 𝑦 ) ( Tr 𝐴 → 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) → ( Tr 𝐴 → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) ) )
15 eleq1w ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) )
16 15 imbi2d ⊢ ( 𝑦 = 𝑧 → ( ( Tr 𝐴 → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( Tr 𝐴 → 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) ) )
17 14 16 frins2 ⊢ ( ( E Fr 𝐴 ∧ E Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( Tr 𝐴 → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
18 1 17 mpan2 ⊢ ( E Fr 𝐴 → ∀ 𝑦 ∈ 𝐴 ( Tr 𝐴 → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
19 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝐴 ( Tr 𝐴 → 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( Tr 𝐴 → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
20 18 19 sylib ⊢ ( E Fr 𝐴 → ( Tr 𝐴 → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
21 dfss3 ⊢ ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
22 20 21 imbitrrdi ⊢ ( E Fr 𝐴 → ( Tr 𝐴 → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) )
23 22 impcom ⊢ ( ( Tr 𝐴 ∧ E Fr 𝐴 ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )