Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  satffunlem1lem2 Structured version   Visualization version   GIF version

Theorem satffunlem1lem2 34690
Description: Lemma 2 for satffunlem1 34694. (Contributed by AV, 23-Oct-2023.)
Assertion
Ref Expression
satffunlem1lem2 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (dom ((𝑀 Sat 𝐸)β€˜βˆ…) ∩ dom {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}))}) = βˆ…)
Distinct variable groups:   𝑓,𝐸,𝑖,𝑒,𝑣,π‘₯,𝑦   𝑓,𝑀,𝑖,𝑒,𝑣,π‘₯,𝑦   𝑓,𝑉,𝑖,𝑒,𝑣,π‘₯   𝑓,π‘Š,𝑖,𝑒,𝑣,π‘₯   π‘₯,𝑗,𝑦
Allowed substitution hints:   𝐸(𝑗)   𝑀(𝑗)   𝑉(𝑦,𝑗)   π‘Š(𝑦,𝑗)

Proof of Theorem satffunlem1lem2
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 peano1 7883 . . . 4 βˆ… ∈ Ο‰
2 satfdmfmla 34687 . . . 4 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ βˆ… ∈ Ο‰) β†’ dom ((𝑀 Sat 𝐸)β€˜βˆ…) = (Fmlaβ€˜βˆ…))
31, 2mp3an3 1448 . . 3 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ dom ((𝑀 Sat 𝐸)β€˜βˆ…) = (Fmlaβ€˜βˆ…))
4 ovex 7446 . . . . . . . . . 10 (𝑀 ↑m Ο‰) ∈ V
54difexi 5329 . . . . . . . . 9 ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V
65a1i 11 . . . . . . . 8 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V)
76ralrimiva 3144 . . . . . . 7 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ βˆ€π‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V)
84rabex 5333 . . . . . . . . 9 {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V
98a1i 11 . . . . . . . 8 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑖 ∈ Ο‰) β†’ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V)
109ralrimiva 3144 . . . . . . 7 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ βˆ€π‘– ∈ Ο‰ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V)
117, 10jca 510 . . . . . 6 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (βˆ€π‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V ∧ βˆ€π‘– ∈ Ο‰ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V))
1211ralrimiva 3144 . . . . 5 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ βˆ€π‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆ€π‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V ∧ βˆ€π‘– ∈ Ο‰ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V))
13 dmopab2rex 5918 . . . . 5 (βˆ€π‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆ€π‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V ∧ βˆ€π‘– ∈ Ο‰ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V) β†’ dom {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}))} = {π‘₯ ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))})
1412, 13syl 17 . . . 4 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ dom {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}))} = {π‘₯ ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))})
15 satfrel 34654 . . . . . . . . . . . . 13 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ βˆ… ∈ Ο‰) β†’ Rel ((𝑀 Sat 𝐸)β€˜βˆ…))
161, 15mp3an3 1448 . . . . . . . . . . . 12 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ Rel ((𝑀 Sat 𝐸)β€˜βˆ…))
17 1stdm 8030 . . . . . . . . . . . 12 ((Rel ((𝑀 Sat 𝐸)β€˜βˆ…) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘’) ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…))
1816, 17sylan 578 . . . . . . . . . . 11 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘’) ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…))
192eqcomd 2736 . . . . . . . . . . . . 13 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ βˆ… ∈ Ο‰) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
201, 19mp3an3 1448 . . . . . . . . . . . 12 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
2120adantr 479 . . . . . . . . . . 11 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
2218, 21eleqtrrd 2834 . . . . . . . . . 10 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘’) ∈ (Fmlaβ€˜βˆ…))
2322adantr 479 . . . . . . . . 9 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ (1st β€˜π‘’) ∈ (Fmlaβ€˜βˆ…))
24 oveq1 7420 . . . . . . . . . . . . 13 (𝑓 = (1st β€˜π‘’) β†’ (π‘“βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”π‘”))
2524eqeq2d 2741 . . . . . . . . . . . 12 (𝑓 = (1st β€˜π‘’) β†’ (π‘₯ = (π‘“βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
2625rexbidv 3176 . . . . . . . . . . 11 (𝑓 = (1st β€˜π‘’) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
27 eqidd 2731 . . . . . . . . . . . . . 14 (𝑓 = (1st β€˜π‘’) β†’ 𝑖 = 𝑖)
28 id 22 . . . . . . . . . . . . . 14 (𝑓 = (1st β€˜π‘’) β†’ 𝑓 = (1st β€˜π‘’))
2927, 28goaleq12d 34638 . . . . . . . . . . . . 13 (𝑓 = (1st β€˜π‘’) β†’ βˆ€π‘”π‘–π‘“ = βˆ€π‘”π‘–(1st β€˜π‘’))
3029eqeq2d 2741 . . . . . . . . . . . 12 (𝑓 = (1st β€˜π‘’) β†’ (π‘₯ = βˆ€π‘”π‘–π‘“ ↔ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
3130rexbidv 3176 . . . . . . . . . . 11 (𝑓 = (1st β€˜π‘’) β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“ ↔ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
3226, 31orbi12d 915 . . . . . . . . . 10 (𝑓 = (1st β€˜π‘’) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
3332adantl 480 . . . . . . . . 9 (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) ∧ 𝑓 = (1st β€˜π‘’)) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
34 1stdm 8030 . . . . . . . . . . . . . . . . 17 ((Rel ((𝑀 Sat 𝐸)β€˜βˆ…) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘£) ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…))
3516, 34sylan 578 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘£) ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…))
3620adantr 479 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
3735, 36eleqtrrd 2834 . . . . . . . . . . . . . . 15 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘£) ∈ (Fmlaβ€˜βˆ…))
3837ad4ant13 747 . . . . . . . . . . . . . 14 (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ (1st β€˜π‘£) ∈ (Fmlaβ€˜βˆ…))
39 oveq2 7421 . . . . . . . . . . . . . . . 16 (𝑔 = (1st β€˜π‘£) β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
4039eqeq2d 2741 . . . . . . . . . . . . . . 15 (𝑔 = (1st β€˜π‘£) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
4140adantl 480 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) ∧ 𝑔 = (1st β€˜π‘£)) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
42 simpr 483 . . . . . . . . . . . . . 14 (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
4338, 41, 42rspcedvd 3615 . . . . . . . . . . . . 13 (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”))
4443ex 411 . . . . . . . . . . . 12 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) β†’ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
4544rexlimdva 3153 . . . . . . . . . . 11 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) β†’ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
4645orim1d 962 . . . . . . . . . 10 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ ((βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
4746imp 405 . . . . . . . . 9 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
4823, 33, 47rspcedvd 3615 . . . . . . . 8 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“))
4948ex 411 . . . . . . 7 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ ((βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
5049rexlimdva 3153 . . . . . 6 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
51 releldm2 8033 . . . . . . . . . 10 (Rel ((𝑀 Sat 𝐸)β€˜βˆ…) β†’ (𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓))
5216, 51syl 17 . . . . . . . . 9 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓))
533eleq2d 2817 . . . . . . . . 9 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ 𝑓 ∈ (Fmlaβ€˜βˆ…)))
5452, 53bitr3d 280 . . . . . . . 8 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓 ↔ 𝑓 ∈ (Fmlaβ€˜βˆ…)))
55 r19.41v 3186 . . . . . . . . . 10 (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) ↔ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
56 oveq1 7420 . . . . . . . . . . . . . . . . 17 ((1st β€˜π‘’) = 𝑓 β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = (π‘“βŠΌπ‘”π‘”))
5756eqeq2d 2741 . . . . . . . . . . . . . . . 16 ((1st β€˜π‘’) = 𝑓 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = (π‘“βŠΌπ‘”π‘”)))
5857rexbidv 3176 . . . . . . . . . . . . . . 15 ((1st β€˜π‘’) = 𝑓 β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”)))
59 eqidd 2731 . . . . . . . . . . . . . . . . . 18 ((1st β€˜π‘’) = 𝑓 β†’ 𝑖 = 𝑖)
60 id 22 . . . . . . . . . . . . . . . . . 18 ((1st β€˜π‘’) = 𝑓 β†’ (1st β€˜π‘’) = 𝑓)
6159, 60goaleq12d 34638 . . . . . . . . . . . . . . . . 17 ((1st β€˜π‘’) = 𝑓 β†’ βˆ€π‘”π‘–(1st β€˜π‘’) = βˆ€π‘”π‘–π‘“)
6261eqeq2d 2741 . . . . . . . . . . . . . . . 16 ((1st β€˜π‘’) = 𝑓 β†’ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ↔ π‘₯ = βˆ€π‘”π‘–π‘“))
6362rexbidv 3176 . . . . . . . . . . . . . . 15 ((1st β€˜π‘’) = 𝑓 β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ↔ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“))
6458, 63orbi12d 915 . . . . . . . . . . . . . 14 ((1st β€˜π‘’) = 𝑓 β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
6564adantl 480 . . . . . . . . . . . . 13 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
663eqcomd 2736 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
6766eleq2d 2817 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑔 ∈ (Fmlaβ€˜βˆ…) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…)))
68 releldm2 8033 . . . . . . . . . . . . . . . . . . . 20 (Rel ((𝑀 Sat 𝐸)β€˜βˆ…) β†’ (𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔))
6916, 68syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔))
7067, 69bitrd 278 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑔 ∈ (Fmlaβ€˜βˆ…) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔))
71 r19.41v 3186 . . . . . . . . . . . . . . . . . . . 20 (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) ↔ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
7239eqcoms 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st β€˜π‘£) = 𝑔 β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
7372eqeq2d 2741 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st β€˜π‘£) = 𝑔 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
7473biimpa 475 . . . . . . . . . . . . . . . . . . . . . 22 (((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
7574a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
7675reximdv 3168 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
7771, 76biimtrrid 242 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ ((βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
7877expd 414 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
7970, 78sylbid 239 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑔 ∈ (Fmlaβ€˜βˆ…) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
8079rexlimdv 3151 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
8180adantr 479 . . . . . . . . . . . . . . 15 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
8281adantr 479 . . . . . . . . . . . . . 14 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (1st β€˜π‘’) = 𝑓) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
8382orim1d 962 . . . . . . . . . . . . 13 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8465, 83sylbird 259 . . . . . . . . . . . 12 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8584expimpd 452 . . . . . . . . . . 11 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8685reximdva 3166 . . . . . . . . . 10 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8755, 86biimtrrid 242 . . . . . . . . 9 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ ((βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8887expd 414 . . . . . . . 8 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓 β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))))
8954, 88sylbird 259 . . . . . . 7 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑓 ∈ (Fmlaβ€˜βˆ…) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))))
9089rexlimdv 3151 . . . . . 6 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
9150, 90impbid 211 . . . . 5 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ↔ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
9291abbidv 2799 . . . 4 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ {π‘₯ ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))} = {π‘₯ ∣ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)})
9314, 92eqtrd 2770 . . 3 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ dom {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}))} = {π‘₯ ∣ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)})
943, 93ineq12d 4214 . 2 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (dom ((𝑀 Sat 𝐸)β€˜βˆ…) ∩ dom {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}))}) = ((Fmlaβ€˜βˆ…) ∩ {π‘₯ ∣ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)}))
95 fmla0disjsuc 34685 . 2 ((Fmlaβ€˜βˆ…) ∩ {π‘₯ ∣ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)}) = βˆ…
9694, 95eqtrdi 2786 1 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (dom ((𝑀 Sat 𝐸)β€˜βˆ…) ∩ dom {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}))}) = βˆ…)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  {cab 2707  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948  βˆ…c0 4323  {csn 4629  βŸ¨cop 4635  {copab 5211  dom cdm 5677   β†Ύ cres 5679  Rel wrel 5682  β€˜cfv 6544  (class class class)co 7413  Ο‰com 7859  1st c1st 7977  2nd c2nd 7978   ↑m cmap 8824  βŠΌπ‘”cgna 34621  βˆ€π‘”cgol 34622   Sat csat 34623  Fmlacfmla 34624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-inf2 9640
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-2o 8471  df-map 8826  df-goel 34627  df-gona 34628  df-goal 34629  df-sat 34630  df-fmla 34632
This theorem is referenced by:  satffunlem1  34694
  Copyright terms: Public domain W3C validator