Metamath Proof Explorer

Theorem trssfir1omregs

Description: If every element in a transitive class is finite, then every element is also hereditarily finite. (Contributed by BTernaryTau, 20-Jan-2026)

Ref Expression
Assertion trssfir1omregs 
|- ( ( Tr A /\ A C_ Fin ) -> A C_ U. ( R1 " _om ) )

Proof

Step Hyp Ref Expression
1 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
2 1 3anbi1d 
 |-  ( x = y -> ( ( x e. A /\ Tr A /\ A C_ Fin ) <-> ( y e. A /\ Tr A /\ A C_ Fin ) ) )
3 eleq1w 
 |-  ( x = y -> ( x e. U. ( R1 " _om ) <-> y e. U. ( R1 " _om ) ) )
4 2 3 imbi12d 
 |-  ( x = y -> ( ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. U. ( R1 " _om ) ) <-> ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. U. ( R1 " _om ) ) ) )
5 ssel2 
 |-  ( ( A C_ Fin /\ x e. A ) -> x e. Fin )
6 5 ancoms 
 |-  ( ( x e. A /\ A C_ Fin ) -> x e. Fin )
7 6 3adant2 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. Fin )
8 7 a1i 
 |-  ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. U. ( R1 " _om ) ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. Fin ) )
9 trel 
 |-  ( Tr A -> ( ( y e. x /\ x e. A ) -> y e. A ) )
10 9 expcomd 
 |-  ( Tr A -> ( x e. A -> ( y e. x -> y e. A ) ) )
11 10 impcom 
 |-  ( ( x e. A /\ Tr A ) -> ( y e. x -> y e. A ) )
12 11 3adant3 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> ( y e. x -> y e. A ) )
13 simp2 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> Tr A )
14 13 a1d 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> ( y e. x -> Tr A ) )
15 simp3 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> A C_ Fin )
16 15 a1d 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> ( y e. x -> A C_ Fin ) )
17 12 14 16 3jcad 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> ( y e. x -> ( y e. A /\ Tr A /\ A C_ Fin ) ) )
18 17 ralrimiv 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> A. y e. x ( y e. A /\ Tr A /\ A C_ Fin ) )
19 ralim 
 |-  ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. U. ( R1 " _om ) ) -> ( A. y e. x ( y e. A /\ Tr A /\ A C_ Fin ) -> A. y e. x y e. U. ( R1 " _om ) ) )
20 18 19 syl5 
 |-  ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. U. ( R1 " _om ) ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> A. y e. x y e. U. ( R1 " _om ) ) )
21 8 20 jcad 
 |-  ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. U. ( R1 " _om ) ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> ( x e. Fin /\ A. y e. x y e. U. ( R1 " _om ) ) ) )
22 r1omhf 
 |-  ( x e. U. ( R1 " _om ) <-> ( x e. Fin /\ A. y e. x y e. U. ( R1 " _om ) ) )
23 21 22 imbitrrdi 
 |-  ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. U. ( R1 " _om ) ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. U. ( R1 " _om ) ) )
24 4 23 setinds2regs 
 |-  ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. U. ( R1 " _om ) )
25 24 3expib 
 |-  ( x e. A -> ( ( Tr A /\ A C_ Fin ) -> x e. U. ( R1 " _om ) ) )
26 25 com12 
 |-  ( ( Tr A /\ A C_ Fin ) -> ( x e. A -> x e. U. ( R1 " _om ) ) )
27 26 ssrdv 
 |-  ( ( Tr A /\ A C_ Fin ) -> A C_ U. ( R1 " _om ) )