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 ( ( ∪ 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
2 ttukey2g ⊢ ( ( ∪ 𝐴 ∈ dom card ∧ 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) )
3 simpr ⊢ ( ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) → ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )
4 3 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )
5 2 4 syl ⊢ ( ( ∪ 𝐴 ∈ dom card ∧ 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )
6 5 3exp ⊢ ( ∪ 𝐴 ∈ dom card → ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) ) )
7 6 exlimdv ⊢ ( ∪ 𝐴 ∈ dom card → ( ∃ 𝑧 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) ) )
8 1 7 biimtrid ⊢ ( ∪ 𝐴 ∈ dom card → ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ) ) )
9 8 3imp ⊢ ( ( ∪ 𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝒫 𝑥 ∩ Fin ) ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 )