Metamath Proof Explorer

Theorem r1omhfbregs

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, 21-Jan-2026)

Ref Expression
Assertion r1omhfbregs 
|- ( 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 df-ral 
 |-  ( A. x e. H A. y e. x y e. H <-> A. x ( x e. H -> A. y e. x y e. H ) )
15 13 14 sylibr 
 |-  ( 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 )
16 dftr5 
 |-  ( Tr H <-> A. x e. H A. y e. x y e. H )
17 15 16 sylibr 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> Tr H )
18 simpl 
 |-  ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. Fin )
19 18 imim2i 
 |-  ( ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> ( x e. H -> x e. Fin ) )
20 19 alimi 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> A. x ( x e. H -> x e. Fin ) )
21 df-ss 
 |-  ( H C_ Fin <-> A. x ( x e. H -> x e. Fin ) )
22 20 21 sylibr 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ Fin )
23 trssfir1omregs 
 |-  ( ( Tr H /\ H C_ Fin ) -> H C_ U. ( R1 " _om ) )
24 17 22 23 syl2anc 
 |-  ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ U. ( R1 " _om ) )
25 10 24 syl 
 |-  ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ U. ( R1 " _om ) )
26 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 ) )
27 26 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 ) )
28 eleq1w 
 |-  ( z = w -> ( z e. U. ( R1 " _om ) <-> w e. U. ( R1 " _om ) ) )
29 eleq1w 
 |-  ( z = w -> ( z e. H <-> w e. H ) )
30 28 29 imbi12d 
 |-  ( z = w -> ( ( z e. U. ( R1 " _om ) -> z e. H ) <-> ( w e. U. ( R1 " _om ) -> w e. H ) ) )
31 30 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 ) ) ) )
32 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 ) ) )
33 r1omhf 
 |-  ( z e. U. ( R1 " _om ) <-> ( z e. Fin /\ A. w e. z w e. U. ( R1 " _om ) ) )
34 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 ) )
35 34 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 ) ) )
36 33 35 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 ) ) )
37 eleq1w 
 |-  ( x = z -> ( x e. Fin <-> z e. Fin ) )
38 eleq1w 
 |-  ( y = w -> ( y e. H <-> w e. H ) )
39 38 adantl 
 |-  ( ( x = z /\ y = w ) -> ( y e. H <-> w e. H ) )
40 simpl 
 |-  ( ( x = z /\ y = w ) -> x = z )
41 39 40 cbvraldva2 
 |-  ( x = z -> ( A. y e. x y e. H <-> A. w e. z w e. H ) )
42 37 41 anbi12d 
 |-  ( x = z -> ( ( x e. Fin /\ A. y e. x y e. H ) <-> ( z e. Fin /\ A. w e. z w e. H ) ) )
43 eleq1w 
 |-  ( x = z -> ( x e. H <-> z e. H ) )
44 42 43 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 ) ) )
45 44 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 ) )
46 36 45 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 ) ) )
47 32 46 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 ) ) )
48 31 47 setinds2regs 
 |-  ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. U. ( R1 " _om ) -> z e. H ) )
49 48 ssrdv 
 |-  ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> U. ( R1 " _om ) C_ H )
50 27 49 syl 
 |-  ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> U. ( R1 " _om ) C_ H )
51 25 50 eqssd 
 |-  ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> H = U. ( R1 " _om ) )
52 8 51 impbii 
 |-  ( H = U. ( R1 " _om ) <-> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) )