Metamath Proof Explorer

Theorem zorn2lem3

Description: Lemma for zorn2 . (Contributed by NM, 3-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses zorn2lem.3 ⊢ F = recs ⁡ f ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u w v
zorn2lem.4 ⊢ C = z ∈ A | ∀ g ∈ ran ⁡ f g R z
zorn2lem.5 ⊢ D = z ∈ A | ∀ g ∈ F x g R z
Assertion zorn2lem3 ⊢ R Po A ∧ x ∈ On ∧ w We A ∧ D ≠ ∅ → y ∈ x → ¬ F ⁡ x = F ⁡ y

Proof

Step Hyp Ref Expression
1 zorn2lem.3 ⊢ F = recs ⁡ f ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u w v
2 zorn2lem.4 ⊢ C = z ∈ A | ∀ g ∈ ran ⁡ f g R z
3 zorn2lem.5 ⊢ D = z ∈ A | ∀ g ∈ F x g R z
4 1 2 3 zorn2lem2 ⊢ x ∈ On ∧ w We A ∧ D ≠ ∅ → y ∈ x → F ⁡ y R F ⁡ x
5 4 adantl ⊢ R Po A ∧ x ∈ On ∧ w We A ∧ D ≠ ∅ → y ∈ x → F ⁡ y R F ⁡ x
6 3 ssrab3 ⊢ D ⊆ A
7 1 2 3 zorn2lem1 ⊢ x ∈ On ∧ w We A ∧ D ≠ ∅ → F ⁡ x ∈ D
8 6 7 sselid ⊢ x ∈ On ∧ w We A ∧ D ≠ ∅ → F ⁡ x ∈ A
9 breq1 ⊢ F ⁡ x = F ⁡ y → F ⁡ x R F ⁡ x ↔ F ⁡ y R F ⁡ x
10 9 biimprcd ⊢ F ⁡ y R F ⁡ x → F ⁡ x = F ⁡ y → F ⁡ x R F ⁡ x
11 poirr ⊢ R Po A ∧ F ⁡ x ∈ A → ¬ F ⁡ x R F ⁡ x
12 10 11 nsyli ⊢ F ⁡ y R F ⁡ x → R Po A ∧ F ⁡ x ∈ A → ¬ F ⁡ x = F ⁡ y
13 12 com12 ⊢ R Po A ∧ F ⁡ x ∈ A → F ⁡ y R F ⁡ x → ¬ F ⁡ x = F ⁡ y
14 8 13 sylan2 ⊢ R Po A ∧ x ∈ On ∧ w We A ∧ D ≠ ∅ → F ⁡ y R F ⁡ x → ¬ F ⁡ x = F ⁡ y
15 5 14 syld ⊢ R Po A ∧ x ∈ On ∧ w We A ∧ D ≠ ∅ → y ∈ x → ¬ F ⁡ x = F ⁡ y