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 \in dom card \land A \neq \emptyset \land \forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A)) \to \exists x \in A \forall y \in A \neg x \subset y$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
2		ttukey2g	$⊢ (⋃ A \in dom card \land z \in A \land \forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A)) \to \exists x \in A (z \subseteq x \land \forall y \in A \neg x \subset y)$
3		simpr	$⊢ (z \subseteq x \land \forall y \in A \neg x \subset y) \to \forall y \in A \neg x \subset y$
4	3	reximi	$⊢ \exists x \in A (z \subseteq x \land \forall y \in A \neg x \subset y) \to \exists x \in A \forall y \in A \neg x \subset y$
5	2 4	syl	$⊢ (⋃ A \in dom card \land z \in A \land \forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A)) \to \exists x \in A \forall y \in A \neg x \subset y$
6	5	3exp	$⊢ ⋃ A \in dom card \to (z \in A \to (\forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A) \to \exists x \in A \forall y \in A \neg x \subset y))$
7	6	exlimdv	$⊢ ⋃ A \in dom card \to (\exists z z \in A \to (\forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A) \to \exists x \in A \forall y \in A \neg x \subset y))$
8	1 7	syl5bi	$⊢ ⋃ A \in dom card \to (A \neq \emptyset \to (\forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A) \to \exists x \in A \forall y \in A \neg x \subset y))$
9	8	3imp	$⊢ (⋃ A \in dom card \land A \neq \emptyset \land \forall x (x \in A \leftrightarrow 𝒫 x \cap Fin \subseteq A)) \to \exists x \in A \forall y \in A \neg x \subset y$