Metamath Proof Explorer

Theorem satfvsuclem1

Description: Lemma 1 for satfvsuc . (Contributed by AV, 8-Oct-2023)

Ref Expression
Hypothesis satfv0.s ⊢S=MSatE
Assertion satfvsuclem1 ⊢M∈V∧E∈W∧N∈ω→xy|∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω∈V

Proof

Step Hyp Ref Expression
1 satfv0.s ⊢S=MSatE
2 ancom ⊢∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω↔y∈𝒫Mω∧∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u
3 2 opabbii ⊢xy|∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω=xy|y∈𝒫Mω∧∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u
4 ovex ⊢Mω∈V
5 4 pwex ⊢𝒫Mω∈V
6 5 a1i ⊢M∈V∧E∈W∧N∈ω→𝒫Mω∈V
7 fvex ⊢S⁡N∈V
8 unab ⊢x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∪x|∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u=x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u
9 7 abrexex ⊢x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∈V
10 simpl ⊢x=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v→x=1st⁡u⊼𝑔1st⁡v
11 10 reximi ⊢∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v→∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v
12 11 ss2abi ⊢x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v⊆x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v
13 9 12 ssexi ⊢x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∈V
14 omex ⊢ω∈V
15 14 abrexex ⊢x|∃i∈ωx=∀𝑔i1st⁡u∈V
16 simpl ⊢x=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u→x=∀𝑔i1st⁡u
17 16 reximi ⊢∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u→∃i∈ωx=∀𝑔i1st⁡u
18 17 ss2abi ⊢x|∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u⊆x|∃i∈ωx=∀𝑔i1st⁡u
19 15 18 ssexi ⊢x|∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V
20 13 19 unex ⊢x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∪x|∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V
21 8 20 eqeltrri ⊢x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V
22 21 a1i ⊢M∈V∧E∈W∧N∈ω∧y∈𝒫Mω∧u∈S⁡N→x|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V
23 22 ralrimiva ⊢M∈V∧E∈W∧N∈ω∧y∈𝒫Mω→∀u∈S⁡Nx|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V
24 abrexex2g ⊢S⁡N∈V∧∀u∈S⁡Nx|∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V→x|∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V
25 7 23 24 sylancr ⊢M∈V∧E∈W∧N∈ω∧y∈𝒫Mω→x|∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V
26 6 25 opabex3rd ⊢M∈V∧E∈W∧N∈ω→xy|y∈𝒫Mω∧∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈V
27 3 26 eqeltrid ⊢M∈V∧E∈W∧N∈ω→xy|∃u∈S⁡N∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω∈V