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 A /\ _E Fr A ) -> A C_ U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 epse 
 |-  _E Se A
2 r19.21v 
 |-  ( A. z e. Pred ( _E , A , y ) ( Tr A -> z e. U. ( R1 " On ) ) <-> ( Tr A -> A. z e. Pred ( _E , A , y ) z e. U. ( R1 " On ) ) )
3 trpred 
 |-  ( ( Tr A /\ y e. A ) -> Pred ( _E , A , y ) = y )
4 raleq 
 |-  ( Pred ( _E , A , y ) = y -> ( A. z e. Pred ( _E , A , y ) z e. U. ( R1 " On ) <-> A. z e. y z e. U. ( R1 " On ) ) )
5 dfss3 
 |-  ( y C_ U. ( R1 " On ) <-> A. z e. y z e. U. ( R1 " On ) )
6 4 5 bitr4di 
 |-  ( Pred ( _E , A , y ) = y -> ( A. z e. Pred ( _E , A , y ) z e. U. ( R1 " On ) <-> y C_ U. ( R1 " On ) ) )
7 vex 
 |-  y e. _V
8 7 r1elss 
 |-  ( y e. U. ( R1 " On ) <-> y C_ U. ( R1 " On ) )
9 6 8 bitr4di 
 |-  ( Pred ( _E , A , y ) = y -> ( A. z e. Pred ( _E , A , y ) z e. U. ( R1 " On ) <-> y e. U. ( R1 " On ) ) )
10 3 9 syl 
 |-  ( ( Tr A /\ y e. A ) -> ( A. z e. Pred ( _E , A , y ) z e. U. ( R1 " On ) <-> y e. U. ( R1 " On ) ) )
11 10 biimpd 
 |-  ( ( Tr A /\ y e. A ) -> ( A. z e. Pred ( _E , A , y ) z e. U. ( R1 " On ) -> y e. U. ( R1 " On ) ) )
12 11 expcom 
 |-  ( y e. A -> ( Tr A -> ( A. z e. Pred ( _E , A , y ) z e. U. ( R1 " On ) -> y e. U. ( R1 " On ) ) ) )
13 12 a2d 
 |-  ( y e. A -> ( ( Tr A -> A. z e. Pred ( _E , A , y ) z e. U. ( R1 " On ) ) -> ( Tr A -> y e. U. ( R1 " On ) ) ) )
14 2 13 biimtrid 
 |-  ( y e. A -> ( A. z e. Pred ( _E , A , y ) ( Tr A -> z e. U. ( R1 " On ) ) -> ( Tr A -> y e. U. ( R1 " On ) ) ) )
15 eleq1w 
 |-  ( y = z -> ( y e. U. ( R1 " On ) <-> z e. U. ( R1 " On ) ) )
16 15 imbi2d 
 |-  ( y = z -> ( ( Tr A -> y e. U. ( R1 " On ) ) <-> ( Tr A -> z e. U. ( R1 " On ) ) ) )
17 14 16 frins2 
 |-  ( ( _E Fr A /\ _E Se A ) -> A. y e. A ( Tr A -> y e. U. ( R1 " On ) ) )
18 1 17 mpan2 
 |-  ( _E Fr A -> A. y e. A ( Tr A -> y e. U. ( R1 " On ) ) )
19 r19.21v 
 |-  ( A. y e. A ( Tr A -> y e. U. ( R1 " On ) ) <-> ( Tr A -> A. y e. A y e. U. ( R1 " On ) ) )
20 18 19 sylib 
 |-  ( _E Fr A -> ( Tr A -> A. y e. A y e. U. ( R1 " On ) ) )
21 dfss3 
 |-  ( A C_ U. ( R1 " On ) <-> A. y e. A y e. U. ( R1 " On ) )
22 20 21 imbitrrdi 
 |-  ( _E Fr A -> ( Tr A -> A C_ U. ( R1 " On ) ) )
23 22 impcom 
 |-  ( ( Tr A /\ _E Fr A ) -> A C_ U. ( R1 " On ) )