Metamath Proof Explorer

Theorem supisoex

Description: Lemma for supiso . (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supiso.1 ⊢ φ → F Isom R , S A B
supiso.2 ⊢ φ → C ⊆ A
supisoex.3 ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z
Assertion supisoex ⊢ φ → ∃ u ∈ B ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v

Proof

Step Hyp Ref Expression
1 supiso.1 ⊢ φ → F Isom R , S A B
2 supiso.2 ⊢ φ → C ⊆ A
3 supisoex.3 ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z
4 simpl ⊢ F Isom R , S A B ∧ C ⊆ A → F Isom R , S A B
5 simpr ⊢ F Isom R , S A B ∧ C ⊆ A → C ⊆ A
6 4 5 supisolem ⊢ F Isom R , S A B ∧ C ⊆ A ∧ x ∈ A → ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z ↔ ∀ w ∈ F C ¬ F ⁡ x S w ∧ ∀ w ∈ B w S F ⁡ x → ∃ v ∈ F C w S v
7 isof1o ⊢ F Isom R , S A B → F : A ⟶ 1-1 onto B
8 f1of ⊢ F : A ⟶ 1-1 onto B → F : A ⟶ B
9 4 7 8 3syl ⊢ F Isom R , S A B ∧ C ⊆ A → F : A ⟶ B
10 9 ffvelcdmda ⊢ F Isom R , S A B ∧ C ⊆ A ∧ x ∈ A → F ⁡ x ∈ B
11 breq1 ⊢ u = F ⁡ x → u S w ↔ F ⁡ x S w
12 11 notbid ⊢ u = F ⁡ x → ¬ u S w ↔ ¬ F ⁡ x S w
13 12 ralbidv ⊢ u = F ⁡ x → ∀ w ∈ F C ¬ u S w ↔ ∀ w ∈ F C ¬ F ⁡ x S w
14 breq2 ⊢ u = F ⁡ x → w S u ↔ w S F ⁡ x
15 14 imbi1d ⊢ u = F ⁡ x → w S u → ∃ v ∈ F C w S v ↔ w S F ⁡ x → ∃ v ∈ F C w S v
16 15 ralbidv ⊢ u = F ⁡ x → ∀ w ∈ B w S u → ∃ v ∈ F C w S v ↔ ∀ w ∈ B w S F ⁡ x → ∃ v ∈ F C w S v
17 13 16 anbi12d ⊢ u = F ⁡ x → ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v ↔ ∀ w ∈ F C ¬ F ⁡ x S w ∧ ∀ w ∈ B w S F ⁡ x → ∃ v ∈ F C w S v
18 17 rspcev ⊢ F ⁡ x ∈ B ∧ ∀ w ∈ F C ¬ F ⁡ x S w ∧ ∀ w ∈ B w S F ⁡ x → ∃ v ∈ F C w S v → ∃ u ∈ B ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v
19 18 ex ⊢ F ⁡ x ∈ B → ∀ w ∈ F C ¬ F ⁡ x S w ∧ ∀ w ∈ B w S F ⁡ x → ∃ v ∈ F C w S v → ∃ u ∈ B ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v
20 10 19 syl ⊢ F Isom R , S A B ∧ C ⊆ A ∧ x ∈ A → ∀ w ∈ F C ¬ F ⁡ x S w ∧ ∀ w ∈ B w S F ⁡ x → ∃ v ∈ F C w S v → ∃ u ∈ B ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v
21 6 20 sylbid ⊢ F Isom R , S A B ∧ C ⊆ A ∧ x ∈ A → ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z → ∃ u ∈ B ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v
22 21 rexlimdva ⊢ F Isom R , S A B ∧ C ⊆ A → ∃ x ∈ A ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z → ∃ u ∈ B ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v
23 1 2 22 syl2anc ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z → ∃ u ∈ B ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v
24 3 23 mpd ⊢ φ → ∃ u ∈ B ∀ w ∈ F C ¬ u S w ∧ ∀ w ∈ B w S u → ∃ v ∈ F C w S v