This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ttukeyg

Description: The Teichmüller-Tukey Lemma ttukey stated with the "choice" as an antecedent (the hypothesis U. A e. dom card says that U. A is well-orderable). (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion ttukeyg ⊢ ⋃ A ∈ dom ⁡ card ∧ A ≠ ∅ ∧ ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y

Proof

Step Hyp Ref Expression
1 n0 ⊢ A ≠ ∅ ↔ ∃ z z ∈ A
2 ttukey2g ⊢ ⋃ A ∈ dom ⁡ card ∧ z ∈ A ∧ ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A → ∃ x ∈ A z ⊆ x ∧ ∀ y ∈ A ¬ x ⊂ y
3 simpr ⊢ z ⊆ x ∧ ∀ y ∈ A ¬ x ⊂ y → ∀ y ∈ A ¬ x ⊂ y
4 3 reximi ⊢ ∃ x ∈ A z ⊆ x ∧ ∀ y ∈ A ¬ x ⊂ y → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y
5 2 4 syl ⊢ ⋃ A ∈ dom ⁡ card ∧ z ∈ A ∧ ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y
6 5 3exp ⊢ ⋃ A ∈ dom ⁡ card → z ∈ A → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y
7 6 exlimdv ⊢ ⋃ A ∈ dom ⁡ card → ∃ z z ∈ A → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y
8 1 7 biimtrid ⊢ ⋃ A ∈ dom ⁡ card → A ≠ ∅ → ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y
9 8 3imp ⊢ ⋃ A ∈ dom ⁡ card ∧ A ≠ ∅ ∧ ∀ x x ∈ A ↔ 𝒫 x ∩ Fin ⊆ A → ∃ x ∈ A ∀ y ∈ A ¬ x ⊂ y