Metamath Proof Explorer

Theorem r1omhfb

Description: The class of all hereditarily finite sets is the only class with the property that all sets are members of it iff they are finite and all of their elements are members of it. (Contributed by BTernaryTau, 24-Jan-2026)

Ref Expression
Assertion r1omhfb 
|- ( H = U. ( R1 " _om ) <-> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) )

Proof

Step Hyp Ref Expression
1 r1omhf 
 |-  ( x e. U. ( R1 " _om ) <-> ( x e. Fin /\ A. y e. x y e. U. ( R1 " _om ) ) )
2 eleq2w2 
 |-  ( H = U. ( R1 " _om ) -> ( x e. H <-> x e. U. ( R1 " _om ) ) )
3 eleq2w2 
 |-  ( H = U. ( R1 " _om ) -> ( y e. H <-> y e. U. ( R1 " _om ) ) )
4 3 ralbidv 
 |-  ( H = U. ( R1 " _om ) -> ( A. y e. x y e. H <-> A. y e. x y e. U. ( R1 " _om ) ) )
5 4 anbi2d 
 |-  ( H = U. ( R1 " _om ) -> ( ( x e. Fin /\ A. y e. x y e. H ) <-> ( x e. Fin /\ A. y e. x y e. U. ( R1 " _om ) ) ) )
6 2 5 bibi12d 
 |-  ( H = U. ( R1 " _om ) -> ( ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) <-> ( x e. U. ( R1 " _om ) <-> ( x e. Fin /\ A. y e. x y e. U. ( R1 " _om ) ) ) ) )
7 1 6 mpbiri 
 |-  ( H = U. ( R1 " _om ) -> ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) )
8 7 alrimiv 
 |-  ( H = U. ( R1 " _om ) -> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) )
9 biimp 
 |-  ( ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) )
10 9 alimi 
 |-  ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) )
11 simpr 
 |-  ( ( x e. Fin /\ A. y e. x y e. H ) -> A. y e. x y e. H )
12 11 imim2i 
 |-  ( ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> ( x e. H -> A. y e. x y e. H ) )
13 12 alimi 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> A. x ( x e. H -> A. y e. x y e. H ) )
14 13 ralrid 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> A. x e. H A. y e. x y e. H )
15 dftr5 
 |-  ( Tr H <-> A. x e. H A. y e. x y e. H )
16 14 15 sylibr 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> Tr H )
17 simpl 
 |-  ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. Fin )
18 17 imim2i 
 |-  ( ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> ( x e. H -> x e. Fin ) )
19 18 alimi 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> A. x ( x e. H -> x e. Fin ) )
20 df-ss 
 |-  ( H C_ Fin <-> A. x ( x e. H -> x e. Fin ) )
21 19 20 sylibr 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ Fin )
22 trssfir1om 
 |-  ( ( Tr H /\ H C_ Fin ) -> H C_ U. ( R1 " _om ) )
23 16 21 22 syl2anc 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ U. ( R1 " _om ) )
24 10 23 syl 
 |-  ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ U. ( R1 " _om ) )
25 biimpr 
 |-  ( ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) )
26 25 alimi 
 |-  ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) )
27 eleq1w 
 |-  ( z = w -> ( z e. U. ( R1 " _om ) <-> w e. U. ( R1 " _om ) ) )
28 eleq1w 
 |-  ( z = w -> ( z e. H <-> w e. H ) )
29 27 28 imbi12d 
 |-  ( z = w -> ( ( z e. U. ( R1 " _om ) -> z e. H ) <-> ( w e. U. ( R1 " _om ) -> w e. H ) ) )
30 29 imbi2d 
 |-  ( z = w -> ( ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. U. ( R1 " _om ) -> z e. H ) ) <-> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. U. ( R1 " _om ) -> w e. H ) ) ) )
31 ra4v 
 |-  ( A. w e. z ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. U. ( R1 " _om ) -> w e. H ) ) -> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> A. w e. z ( w e. U. ( R1 " _om ) -> w e. H ) ) )
32 r1omhf 
 |-  ( z e. U. ( R1 " _om ) <-> ( z e. Fin /\ A. w e. z w e. U. ( R1 " _om ) ) )
33 ralim 
 |-  ( A. w e. z ( w e. U. ( R1 " _om ) -> w e. H ) -> ( A. w e. z w e. U. ( R1 " _om ) -> A. w e. z w e. H ) )
34 33 anim2d 
 |-  ( A. w e. z ( w e. U. ( R1 " _om ) -> w e. H ) -> ( ( z e. Fin /\ A. w e. z w e. U. ( R1 " _om ) ) -> ( z e. Fin /\ A. w e. z w e. H ) ) )
35 32 34 biimtrid 
 |-  ( A. w e. z ( w e. U. ( R1 " _om ) -> w e. H ) -> ( z e. U. ( R1 " _om ) -> ( z e. Fin /\ A. w e. z w e. H ) ) )
36 eleq1w 
 |-  ( x = z -> ( x e. Fin <-> z e. Fin ) )
37 eleq1w 
 |-  ( y = w -> ( y e. H <-> w e. H ) )
38 37 adantl 
 |-  ( ( x = z /\ y = w ) -> ( y e. H <-> w e. H ) )
39 simpl 
 |-  ( ( x = z /\ y = w ) -> x = z )
40 38 39 cbvraldva2 
 |-  ( x = z -> ( A. y e. x y e. H <-> A. w e. z w e. H ) )
41 36 40 anbi12d 
 |-  ( x = z -> ( ( x e. Fin /\ A. y e. x y e. H ) <-> ( z e. Fin /\ A. w e. z w e. H ) ) )
42 eleq1w 
 |-  ( x = z -> ( x e. H <-> z e. H ) )
43 41 42 imbi12d 
 |-  ( x = z -> ( ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) <-> ( ( z e. Fin /\ A. w e. z w e. H ) -> z e. H ) ) )
44 43 spvv 
 |-  ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( ( z e. Fin /\ A. w e. z w e. H ) -> z e. H ) )
45 35 44 syl9r 
 |-  ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( A. w e. z ( w e. U. ( R1 " _om ) -> w e. H ) -> ( z e. U. ( R1 " _om ) -> z e. H ) ) )
46 31 45 sylcom 
 |-  ( A. w e. z ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. U. ( R1 " _om ) -> w e. H ) ) -> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. U. ( R1 " _om ) -> z e. H ) ) )
47 30 46 setinds2 
 |-  ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. U. ( R1 " _om ) -> z e. H ) )
48 47 ssrdv 
 |-  ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> U. ( R1 " _om ) C_ H )
49 26 48 syl 
 |-  ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> U. ( R1 " _om ) C_ H )
50 24 49 eqssd 
 |-  ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> H = U. ( R1 " _om ) )
51 8 50 impbii 
 |-  ( H = U. ( R1 " _om ) <-> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) )