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 34061
Description: Lemma 2 for satffunlem1 34065. (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 7829 . . . 4 βˆ… ∈ Ο‰
2 satfdmfmla 34058 . . . 4 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ βˆ… ∈ Ο‰) β†’ dom ((𝑀 Sat 𝐸)β€˜βˆ…) = (Fmlaβ€˜βˆ…))
31, 2mp3an3 1451 . . 3 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ dom ((𝑀 Sat 𝐸)β€˜βˆ…) = (Fmlaβ€˜βˆ…))
4 ovex 7394 . . . . . . . . . 10 (𝑀 ↑m Ο‰) ∈ V
54difexi 5289 . . . . . . . . 9 ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V
65a1i 11 . . . . . . . 8 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V)
76ralrimiva 3140 . . . . . . 7 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ βˆ€π‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V)
84rabex 5293 . . . . . . . . 9 {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V
98a1i 11 . . . . . . . 8 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑖 ∈ Ο‰) β†’ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V)
109ralrimiva 3140 . . . . . . 7 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ βˆ€π‘– ∈ Ο‰ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V)
117, 10jca 513 . . . . . 6 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (βˆ€π‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V ∧ βˆ€π‘– ∈ Ο‰ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V))
1211ralrimiva 3140 . . . . 5 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ βˆ€π‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆ€π‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V ∧ βˆ€π‘– ∈ Ο‰ {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)} ∈ V))
13 dmopab2rex 5877 . . . . 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 34025 . . . . . . . . . . . . 13 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ βˆ… ∈ Ο‰) β†’ Rel ((𝑀 Sat 𝐸)β€˜βˆ…))
161, 15mp3an3 1451 . . . . . . . . . . . 12 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ Rel ((𝑀 Sat 𝐸)β€˜βˆ…))
17 1stdm 7976 . . . . . . . . . . . 12 ((Rel ((𝑀 Sat 𝐸)β€˜βˆ…) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘’) ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…))
1816, 17sylan 581 . . . . . . . . . . 11 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘’) ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…))
192eqcomd 2739 . . . . . . . . . . . . 13 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ βˆ… ∈ Ο‰) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
201, 19mp3an3 1451 . . . . . . . . . . . 12 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
2120adantr 482 . . . . . . . . . . 11 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
2218, 21eleqtrrd 2837 . . . . . . . . . 10 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘’) ∈ (Fmlaβ€˜βˆ…))
2322adantr 482 . . . . . . . . 9 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ (1st β€˜π‘’) ∈ (Fmlaβ€˜βˆ…))
24 oveq1 7368 . . . . . . . . . . . . 13 (𝑓 = (1st β€˜π‘’) β†’ (π‘“βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”π‘”))
2524eqeq2d 2744 . . . . . . . . . . . 12 (𝑓 = (1st β€˜π‘’) β†’ (π‘₯ = (π‘“βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
2625rexbidv 3172 . . . . . . . . . . 11 (𝑓 = (1st β€˜π‘’) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
27 eqidd 2734 . . . . . . . . . . . . . 14 (𝑓 = (1st β€˜π‘’) β†’ 𝑖 = 𝑖)
28 id 22 . . . . . . . . . . . . . 14 (𝑓 = (1st β€˜π‘’) β†’ 𝑓 = (1st β€˜π‘’))
2927, 28goaleq12d 34009 . . . . . . . . . . . . 13 (𝑓 = (1st β€˜π‘’) β†’ βˆ€π‘”π‘–π‘“ = βˆ€π‘”π‘–(1st β€˜π‘’))
3029eqeq2d 2744 . . . . . . . . . . . 12 (𝑓 = (1st β€˜π‘’) β†’ (π‘₯ = βˆ€π‘”π‘–π‘“ ↔ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
3130rexbidv 3172 . . . . . . . . . . 11 (𝑓 = (1st β€˜π‘’) β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“ ↔ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
3226, 31orbi12d 918 . . . . . . . . . 10 (𝑓 = (1st β€˜π‘’) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
3332adantl 483 . . . . . . . . 9 (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) ∧ 𝑓 = (1st β€˜π‘’)) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
34 1stdm 7976 . . . . . . . . . . . . . . . . 17 ((Rel ((𝑀 Sat 𝐸)β€˜βˆ…) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘£) ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…))
3516, 34sylan 581 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘£) ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…))
3620adantr 482 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
3735, 36eleqtrrd 2837 . . . . . . . . . . . . . . 15 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (1st β€˜π‘£) ∈ (Fmlaβ€˜βˆ…))
3837ad4ant13 750 . . . . . . . . . . . . . 14 (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ (1st β€˜π‘£) ∈ (Fmlaβ€˜βˆ…))
39 oveq2 7369 . . . . . . . . . . . . . . . 16 (𝑔 = (1st β€˜π‘£) β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
4039eqeq2d 2744 . . . . . . . . . . . . . . 15 (𝑔 = (1st β€˜π‘£) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
4140adantl 483 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) ∧ 𝑔 = (1st β€˜π‘£)) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
42 simpr 486 . . . . . . . . . . . . . 14 (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
4338, 41, 42rspcedvd 3585 . . . . . . . . . . . . 13 (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”))
4443ex 414 . . . . . . . . . . . 12 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) β†’ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
4544rexlimdva 3149 . . . . . . . . . . 11 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) β†’ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
4645orim1d 965 . . . . . . . . . 10 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ ((βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
4746imp 408 . . . . . . . . 9 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
4823, 33, 47rspcedvd 3585 . . . . . . . 8 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“))
4948ex 414 . . . . . . 7 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ ((βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
5049rexlimdva 3149 . . . . . 6 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
51 releldm2 7979 . . . . . . . . . 10 (Rel ((𝑀 Sat 𝐸)β€˜βˆ…) β†’ (𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓))
5216, 51syl 17 . . . . . . . . 9 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓))
533eleq2d 2820 . . . . . . . . 9 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ 𝑓 ∈ (Fmlaβ€˜βˆ…)))
5452, 53bitr3d 281 . . . . . . . 8 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓 ↔ 𝑓 ∈ (Fmlaβ€˜βˆ…)))
55 r19.41v 3182 . . . . . . . . . 10 (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) ↔ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
56 oveq1 7368 . . . . . . . . . . . . . . . . 17 ((1st β€˜π‘’) = 𝑓 β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = (π‘“βŠΌπ‘”π‘”))
5756eqeq2d 2744 . . . . . . . . . . . . . . . 16 ((1st β€˜π‘’) = 𝑓 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = (π‘“βŠΌπ‘”π‘”)))
5857rexbidv 3172 . . . . . . . . . . . . . . 15 ((1st β€˜π‘’) = 𝑓 β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”)))
59 eqidd 2734 . . . . . . . . . . . . . . . . . 18 ((1st β€˜π‘’) = 𝑓 β†’ 𝑖 = 𝑖)
60 id 22 . . . . . . . . . . . . . . . . . 18 ((1st β€˜π‘’) = 𝑓 β†’ (1st β€˜π‘’) = 𝑓)
6159, 60goaleq12d 34009 . . . . . . . . . . . . . . . . 17 ((1st β€˜π‘’) = 𝑓 β†’ βˆ€π‘”π‘–(1st β€˜π‘’) = βˆ€π‘”π‘–π‘“)
6261eqeq2d 2744 . . . . . . . . . . . . . . . 16 ((1st β€˜π‘’) = 𝑓 β†’ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ↔ π‘₯ = βˆ€π‘”π‘–π‘“))
6362rexbidv 3172 . . . . . . . . . . . . . . 15 ((1st β€˜π‘’) = 𝑓 β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ↔ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“))
6458, 63orbi12d 918 . . . . . . . . . . . . . 14 ((1st β€˜π‘’) = 𝑓 β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
6564adantl 483 . . . . . . . . . . . . 13 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
663eqcomd 2739 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (Fmlaβ€˜βˆ…) = dom ((𝑀 Sat 𝐸)β€˜βˆ…))
6766eleq2d 2820 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑔 ∈ (Fmlaβ€˜βˆ…) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…)))
68 releldm2 7979 . . . . . . . . . . . . . . . . . . . 20 (Rel ((𝑀 Sat 𝐸)β€˜βˆ…) β†’ (𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔))
6916, 68syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜βˆ…) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔))
7067, 69bitrd 279 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑔 ∈ (Fmlaβ€˜βˆ…) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔))
71 r19.41v 3182 . . . . . . . . . . . . . . . . . . . 20 (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) ↔ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
7239eqcoms 2741 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st β€˜π‘£) = 𝑔 β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
7372eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st β€˜π‘£) = 𝑔 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
7473biimpa 478 . . . . . . . . . . . . . . . . . . . . . 22 (((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
7574a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
7675reximdv 3164 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
7771, 76biimtrrid 242 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ ((βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
7877expd 417 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘£) = 𝑔 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
7970, 78sylbid 239 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑔 ∈ (Fmlaβ€˜βˆ…) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
8079rexlimdv 3147 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
8180adantr 482 . . . . . . . . . . . . . . 15 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
8281adantr 482 . . . . . . . . . . . . . 14 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (1st β€˜π‘’) = 𝑓) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
8382orim1d 965 . . . . . . . . . . . . 13 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8465, 83sylbird 260 . . . . . . . . . . . 12 ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8584expimpd 455 . . . . . . . . . . 11 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ 𝑒 ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)) β†’ (((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8685reximdva 3162 . . . . . . . . . 10 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8755, 86biimtrrid 242 . . . . . . . . 9 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ ((βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
8887expd 417 . . . . . . . 8 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(1st β€˜π‘’) = 𝑓 β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))))
8954, 88sylbird 260 . . . . . . 7 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (𝑓 ∈ (Fmlaβ€˜βˆ…) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))))
9089rexlimdv 3147 . . . . . 6 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
9150, 90impbid 211 . . . . 5 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ↔ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
9291abbidv 2802 . . . 4 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ {π‘₯ ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))} = {π‘₯ ∣ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)})
9314, 92eqtrd 2773 . . 3 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ dom {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}))} = {π‘₯ ∣ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)})
943, 93ineq12d 4177 . 2 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) β†’ (dom ((𝑀 Sat 𝐸)β€˜βˆ…) ∩ dom {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜βˆ…)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘— ∈ 𝑀 ({βŸ¨π‘–, π‘—βŸ©} βˆͺ (𝑓 β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}))}) = ((Fmlaβ€˜βˆ…) ∩ {π‘₯ ∣ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)}))
95 fmla0disjsuc 34056 . 2 ((Fmlaβ€˜βˆ…) ∩ {π‘₯ ∣ βˆƒπ‘“ ∈ (Fmlaβ€˜βˆ…)(βˆƒπ‘” ∈ (Fmlaβ€˜βˆ…)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)}) = βˆ…
9694, 95eqtrdi 2789 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 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3447   βˆ– cdif 3911   βˆͺ cun 3912   ∩ cin 3913  βˆ…c0 4286  {csn 4590  βŸ¨cop 4596  {copab 5171  dom cdm 5637   β†Ύ cres 5639  Rel wrel 5642  β€˜cfv 6500  (class class class)co 7361  Ο‰com 7806  1st c1st 7923  2nd c2nd 7924   ↑m cmap 8771  βŠΌπ‘”cgna 33992  βˆ€π‘”cgol 33993   Sat csat 33994  Fmlacfmla 33995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-map 8773  df-goel 33998  df-gona 33999  df-goal 34000  df-sat 34001  df-fmla 34003
This theorem is referenced by:  satffunlem1  34065
  Copyright terms: Public domain W3C validator