Metamath Proof Explorer

Theorem satfvsuclem2

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

Ref Expression
Hypothesis satfv0.s ⊢S=MSatE
Assertion satfvsuclem2 ⊢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∈V

Proof

Step Hyp Ref Expression
1 satfv0.s ⊢S=MSatE
2 r19.41v ⊢∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω↔∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω
3 r19.41v ⊢∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω↔∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω
4 2 3 orbi12i ⊢∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω↔∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω
5 ovex ⊢Mω∈V
6 difelpw ⊢Mω∈V→Mω∖2nd⁡u∩2nd⁡v∈𝒫Mω
7 5 6 ax-mp ⊢Mω∖2nd⁡u∩2nd⁡v∈𝒫Mω
8 eleq1 ⊢y=Mω∖2nd⁡u∩2nd⁡v→y∈𝒫Mω↔Mω∖2nd⁡u∩2nd⁡v∈𝒫Mω
9 7 8 mpbiri ⊢y=Mω∖2nd⁡u∩2nd⁡v→y∈𝒫Mω
10 9 pm4.71i ⊢y=Mω∖2nd⁡u∩2nd⁡v↔y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω
11 10 bianass ⊢x=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v↔x=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω
12 11 rexbii ⊢∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v↔∃v∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω
13 rabelpw ⊢Mω∈V→a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈𝒫Mω
14 5 13 ax-mp ⊢a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈𝒫Mω
15 eleq1 ⊢y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u→y∈𝒫Mω↔a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∈𝒫Mω
16 14 15 mpbiri ⊢y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u→y∈𝒫Mω
17 16 pm4.71i ⊢y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u↔y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω
18 17 bianass ⊢x=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u↔x=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω
19 18 rexbii ⊢∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u↔∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω
20 12 19 orbi12i ⊢∃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∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω
21 andir ⊢∃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∈S⁡Nx=1st⁡u⊼𝑔1st⁡v∧y=Mω∖2nd⁡u∩2nd⁡v∧y∈𝒫Mω∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈Mω|∀z∈Miz∪a↾ω∖i∈2nd⁡u∧y∈𝒫Mω
22 4 20 21 3bitr4i ⊢∃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∈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ω
23 22 rexbii ⊢∃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↔∃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ω
24 r19.41v ⊢∃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ω↔∃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ω
25 23 24 bitri ⊢∃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↔∃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ω
26 25 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=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ω
27 1 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
28 26 27 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∈V