Description: The hypothesis of this theorem defines a class M of sets that we temporarily call "minimal universes", and which will turn out in grumnueq to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on y in rr-groth , except for the x e. y clause.
A minimal universe is closed under subsets ( mnussd ), powersets ( mnupwd ), and an operation which is similar to a combination of collection and union ( mnuop3d ), from which closure under pairing ( mnuprd ), unions ( mnuunid ), and function ranges ( mnurnd ) can be deduced, from which equivalence with Grothendieck universes ( grumnueq ) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ismnu.1 | ⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) } | |
| Assertion | ismnu | ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ 𝑀 ↔ ∀ 𝑧 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ismnu.1 | ⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) } | |
| 2 | simpr | ⊢ ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ) → 𝑙 = 𝑧 ) | |
| 3 | 2 | pweqd | ⊢ ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ) → 𝒫 𝑙 = 𝒫 𝑧 ) |
| 4 | simpl | ⊢ ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ) → 𝑘 = 𝑈 ) | |
| 5 | 3 4 | sseq12d | ⊢ ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ) → ( 𝒫 𝑙 ⊆ 𝑘 ↔ 𝒫 𝑧 ⊆ 𝑈 ) ) |
| 6 | 3 | 3adant3 | ⊢ ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) → 𝒫 𝑙 = 𝒫 𝑧 ) |
| 7 | 6 | adantr | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ) → 𝒫 𝑙 = 𝒫 𝑧 ) |
| 8 | simpr | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ) → 𝑛 = 𝑤 ) | |
| 9 | 7 8 | sseq12d | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ) → ( 𝒫 𝑙 ⊆ 𝑛 ↔ 𝒫 𝑧 ⊆ 𝑤 ) ) |
| 10 | simpl3 | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑞 = 𝑣 ) → 𝑝 = 𝑖 ) | |
| 11 | simpr | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑞 = 𝑣 ) → 𝑞 = 𝑣 ) | |
| 12 | 10 11 | eleq12d | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑞 = 𝑣 ) → ( 𝑝 ∈ 𝑞 ↔ 𝑖 ∈ 𝑣 ) ) |
| 13 | simpl13 | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑞 = 𝑣 ) → 𝑚 = 𝑓 ) | |
| 14 | 11 13 | eleq12d | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑞 = 𝑣 ) → ( 𝑞 ∈ 𝑚 ↔ 𝑣 ∈ 𝑓 ) ) |
| 15 | 12 14 | anbi12d | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑞 = 𝑣 ) → ( ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) ↔ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ) |
| 16 | simpl11 | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑞 = 𝑣 ) → 𝑘 = 𝑈 ) | |
| 17 | 15 16 | cbvrexdva2 | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) → ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ) |
| 18 | simpl3 | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑟 = 𝑢 ) → 𝑝 = 𝑖 ) | |
| 19 | simpr | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑟 = 𝑢 ) → 𝑟 = 𝑢 ) | |
| 20 | 18 19 | eleq12d | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑟 = 𝑢 ) → ( 𝑝 ∈ 𝑟 ↔ 𝑖 ∈ 𝑢 ) ) |
| 21 | 19 | unieqd | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑟 = 𝑢 ) → ∪ 𝑟 = ∪ 𝑢 ) |
| 22 | simpl2 | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑟 = 𝑢 ) → 𝑛 = 𝑤 ) | |
| 23 | 21 22 | sseq12d | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑟 = 𝑢 ) → ( ∪ 𝑟 ⊆ 𝑛 ↔ ∪ 𝑢 ⊆ 𝑤 ) ) |
| 24 | 20 23 | anbi12d | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑟 = 𝑢 ) → ( ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ↔ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) |
| 25 | simpl13 | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) ∧ 𝑟 = 𝑢 ) → 𝑚 = 𝑓 ) | |
| 26 | 24 25 | cbvrexdva2 | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) → ( ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ↔ ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) |
| 27 | 17 26 | imbi12d | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖 ) → ( ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ↔ ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) |
| 28 | 27 | 3expa | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ) ∧ 𝑝 = 𝑖 ) → ( ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ↔ ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) |
| 29 | simpll2 | ⊢ ( ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ) ∧ 𝑝 = 𝑖 ) → 𝑙 = 𝑧 ) | |
| 30 | 28 29 | cbvraldva2 | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ) → ( ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ↔ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) |
| 31 | 9 30 | anbi12d | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ) → ( ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ↔ ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
| 32 | simpl1 | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) ∧ 𝑛 = 𝑤 ) → 𝑘 = 𝑈 ) | |
| 33 | 31 32 | cbvrexdva2 | ⊢ ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓 ) → ( ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ↔ ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
| 34 | 33 | 3expa | ⊢ ( ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ) ∧ 𝑚 = 𝑓 ) → ( ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ↔ ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
| 35 | 34 | cbvaldvaw | ⊢ ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ) → ( ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ↔ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
| 36 | 5 35 | anbi12d | ⊢ ( ( 𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ) → ( ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) ↔ ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) ) |
| 37 | 36 4 | cbvraldva2 | ⊢ ( 𝑘 = 𝑈 → ( ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) ↔ ∀ 𝑧 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) ) |
| 38 | 37 1 | elab2g | ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ 𝑀 ↔ ∀ 𝑧 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) ) |