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 ( 𝐻 = ∪ ( 𝑅1 “ ω ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 r1omhf ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) )
2 eleq2w2 ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) → ( 𝑥 ∈ 𝐻 ↔ 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) )
3 eleq2w2 ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) → ( 𝑦 ∈ 𝐻 ↔ 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) )
4 3 ralbidv ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) )
5 4 anbi2d ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) → ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) ) )
6 2 5 bibi12d ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) → ( ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) ↔ ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) ) ) )
7 1 6 mpbiri ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) → ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) )
8 7 alrimiv ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) → ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) )
9 biimp ⊢ ( ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) )
10 9 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) )
11 simpr ⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 )
12 11 imim2i ⊢ ( ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ∈ 𝐻 → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) )
13 12 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) )
14 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) )
15 13 14 sylibr ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 )
16 dftr5 ⊢ ( Tr 𝐻 ↔ ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 )
17 15 16 sylibr ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → Tr 𝐻 )
18 simpl ⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ Fin )
19 18 imim2i ⊢ ( ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ∈ 𝐻 → 𝑥 ∈ Fin ) )
20 19 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐻 → 𝑥 ∈ Fin ) )
21 df-ss ⊢ ( 𝐻 ⊆ Fin ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐻 → 𝑥 ∈ Fin ) )
22 20 21 sylibr ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → 𝐻 ⊆ Fin )
23 trssfir1omregs ⊢ ( ( Tr 𝐻 ∧ 𝐻 ⊆ Fin ) → 𝐻 ⊆ ∪ ( 𝑅1 “ ω ) )
24 17 22 23 syl2anc ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → 𝐻 ⊆ ∪ ( 𝑅1 “ ω ) )
25 10 24 syl ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → 𝐻 ⊆ ∪ ( 𝑅1 “ ω ) )
26 biimpr ⊢ ( ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) )
27 26 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) )
28 eleq1w ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) ↔ 𝑤 ∈ ∪ ( 𝑅1 “ ω ) ) )
29 eleq1w ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ 𝐻 ↔ 𝑤 ∈ 𝐻 ) )
30 28 29 imbi12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) ↔ ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) )
31 30 imbi2d ⊢ ( 𝑧 = 𝑤 → ( ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) ) ↔ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) ) )
32 ra4v ⊢ ( ∀ 𝑤 ∈ 𝑧 ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) → ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) )
33 r1omhf ⊢ ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) ↔ ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ ∪ ( 𝑅1 “ ω ) ) )
34 ralim ⊢ ( ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) → ( ∀ 𝑤 ∈ 𝑧 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) )
35 34 anim2d ⊢ ( ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) → ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ ∪ ( 𝑅1 “ ω ) ) → ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) ) )
36 33 35 biimtrid ⊢ ( ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) ) )
37 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ Fin ↔ 𝑧 ∈ Fin ) )
38 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐻 ↔ 𝑤 ∈ 𝐻 ) )
39 38 adantl ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝐻 ↔ 𝑤 ∈ 𝐻 ) )
40 simpl ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑥 = 𝑧 )
41 39 40 cbvraldva2 ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ↔ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) )
42 37 41 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ↔ ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) ) )
43 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐻 ↔ 𝑧 ∈ 𝐻 ) )
44 42 43 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) ↔ ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) → 𝑧 ∈ 𝐻 ) ) )
45 44 spvv ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) → 𝑧 ∈ 𝐻 ) )
46 36 45 syl9r ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) ) )
47 32 46 sylcom ⊢ ( ∀ 𝑤 ∈ 𝑧 ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) → ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) ) )
48 31 47 setinds2regs ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) )
49 48 ssrdv ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ∪ ( 𝑅1 “ ω ) ⊆ 𝐻 )
50 27 49 syl ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∪ ( 𝑅1 “ ω ) ⊆ 𝐻 )
51 25 50 eqssd ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → 𝐻 = ∪ ( 𝑅1 “ ω ) )
52 8 51 impbii ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) )