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