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 ( 𝐻 = ∪ ( 𝑅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 13 ralrid ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 )
15 dftr5 ⊢ ( Tr 𝐻 ↔ ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 )
16 14 15 sylibr ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → Tr 𝐻 )
17 simpl ⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ Fin )
18 17 imim2i ⊢ ( ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ∈ 𝐻 → 𝑥 ∈ Fin ) )
19 18 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐻 → 𝑥 ∈ Fin ) )
20 df-ss ⊢ ( 𝐻 ⊆ Fin ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐻 → 𝑥 ∈ Fin ) )
21 19 20 sylibr ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → 𝐻 ⊆ Fin )
22 trssfir1om ⊢ ( ( Tr 𝐻 ∧ 𝐻 ⊆ Fin ) → 𝐻 ⊆ ∪ ( 𝑅1 “ ω ) )
23 16 21 22 syl2anc ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → 𝐻 ⊆ ∪ ( 𝑅1 “ ω ) )
24 10 23 syl ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → 𝐻 ⊆ ∪ ( 𝑅1 “ ω ) )
25 biimpr ⊢ ( ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) )
26 25 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) )
27 eleq1w ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) ↔ 𝑤 ∈ ∪ ( 𝑅1 “ ω ) ) )
28 eleq1w ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ 𝐻 ↔ 𝑤 ∈ 𝐻 ) )
29 27 28 imbi12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) ↔ ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) )
30 29 imbi2d ⊢ ( 𝑧 = 𝑤 → ( ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) ) ↔ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) ) )
31 ra4v ⊢ ( ∀ 𝑤 ∈ 𝑧 ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) → ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) )
32 r1omhf ⊢ ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) ↔ ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ ∪ ( 𝑅1 “ ω ) ) )
33 ralim ⊢ ( ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) → ( ∀ 𝑤 ∈ 𝑧 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) )
34 33 anim2d ⊢ ( ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) → ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ ∪ ( 𝑅1 “ ω ) ) → ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) ) )
35 32 34 biimtrid ⊢ ( ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) ) )
36 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ Fin ↔ 𝑧 ∈ Fin ) )
37 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐻 ↔ 𝑤 ∈ 𝐻 ) )
38 37 adantl ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝐻 ↔ 𝑤 ∈ 𝐻 ) )
39 simpl ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑥 = 𝑧 )
40 38 39 cbvraldva2 ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ↔ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) )
41 36 40 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ↔ ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) ) )
42 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐻 ↔ 𝑧 ∈ 𝐻 ) )
43 41 42 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) ↔ ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) → 𝑧 ∈ 𝐻 ) ) )
44 43 spvv ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ∈ 𝐻 ) → 𝑧 ∈ 𝐻 ) )
45 35 44 syl9r ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( ∀ 𝑤 ∈ 𝑧 ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) ) )
46 31 45 sylcom ⊢ ( ∀ 𝑤 ∈ 𝑧 ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑤 ∈ ∪ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝐻 ) ) → ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) ) )
47 30 46 setinds2 ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ( 𝑧 ∈ ∪ ( 𝑅1 “ ω ) → 𝑧 ∈ 𝐻 ) )
48 47 ssrdv ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 ) → ∪ ( 𝑅1 “ ω ) ⊆ 𝐻 )
49 26 48 syl ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → ∪ ( 𝑅1 “ ω ) ⊆ 𝐻 )
50 24 49 eqssd ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) → 𝐻 = ∪ ( 𝑅1 “ ω ) )
51 8 50 impbii ⊢ ( 𝐻 = ∪ ( 𝑅1 “ ω ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐻 ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐻 ) ) )