Metamath Proof Explorer

Theorem satfvsuclem2

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

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

Proof

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