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

Theorem satffunlem2lem2 34064
Description: Lemma 2 for satffunlem2 34066. (Contributed by AV, 27-Oct-2023.)
Hypotheses
Ref Expression
satffunlem2lem2.s 𝑆 = (𝑀 Sat 𝐸)
satffunlem2lem2.a 𝐴 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))
satffunlem2lem2.b 𝐡 = {π‘Ž ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘§ ∈ 𝑀 ({βŸ¨π‘–, π‘§βŸ©} βˆͺ (π‘Ž β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}
Assertion
Ref Expression
satffunlem2lem2 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (dom (π‘†β€˜suc 𝑁) ∩ dom {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = 𝐡)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴))}) = βˆ…)
Distinct variable groups:   𝐴,𝑖,π‘₯,𝑦   π‘₯,𝐡,𝑦   𝑖,𝐸,𝑒,𝑣,π‘₯   𝑀,π‘Ž   𝑖,𝑀,𝑒,𝑣,π‘₯   𝑖,𝑁,𝑒,𝑣,π‘₯,𝑦   𝑆,𝑖,𝑒,𝑣,π‘₯,𝑦   𝑖,𝑉,𝑒,𝑣,π‘₯   𝑖,π‘Š,𝑒,𝑣,π‘₯
Allowed substitution hints:   𝐴(𝑧,𝑣,𝑒,π‘Ž)   𝐡(𝑧,𝑣,𝑒,𝑖,π‘Ž)   𝑆(𝑧,π‘Ž)   𝐸(𝑦,𝑧,π‘Ž)   𝑀(𝑦,𝑧)   𝑁(𝑧,π‘Ž)   𝑉(𝑦,𝑧,π‘Ž)   π‘Š(𝑦,𝑧,π‘Ž)

Proof of Theorem satffunlem2lem2
Dummy variables 𝑓 𝑔 𝑑 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 satffunlem2lem2.s . . . . . 6 𝑆 = (𝑀 Sat 𝐸)
21fveq1i 6847 . . . . 5 (π‘†β€˜suc 𝑁) = ((𝑀 Sat 𝐸)β€˜suc 𝑁)
32dmeqi 5864 . . . 4 dom (π‘†β€˜suc 𝑁) = dom ((𝑀 Sat 𝐸)β€˜suc 𝑁)
4 simprl 770 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ 𝑀 ∈ 𝑉)
5 simprr 772 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ 𝐸 ∈ π‘Š)
6 peano2 7831 . . . . . . . 8 (𝑁 ∈ Ο‰ β†’ suc 𝑁 ∈ Ο‰)
76adantr 482 . . . . . . 7 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ suc 𝑁 ∈ Ο‰)
84, 5, 73jca 1129 . . . . . 6 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ suc 𝑁 ∈ Ο‰))
9 satfdmfmla 34058 . . . . . 6 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ suc 𝑁 ∈ Ο‰) β†’ dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) = (Fmlaβ€˜suc 𝑁))
108, 9syl 17 . . . . 5 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) = (Fmlaβ€˜suc 𝑁))
1110adantr 482 . . . 4 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) = (Fmlaβ€˜suc 𝑁))
123, 11eqtrid 2785 . . 3 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ dom (π‘†β€˜suc 𝑁) = (Fmlaβ€˜suc 𝑁))
13 satffunlem2lem2.a . . . . . . . . . 10 𝐴 = ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£)))
14 ovex 7394 . . . . . . . . . . 11 (𝑀 ↑m Ο‰) ∈ V
1514difexi 5289 . . . . . . . . . 10 ((𝑀 ↑m Ο‰) βˆ– ((2nd β€˜π‘’) ∩ (2nd β€˜π‘£))) ∈ V
1613, 15eqeltri 2830 . . . . . . . . 9 𝐴 ∈ V
1716a1i 11 . . . . . . . 8 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) β†’ 𝐴 ∈ V)
1817ralrimiva 3140 . . . . . . 7 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜suc 𝑁)) β†’ βˆ€π‘£ ∈ (π‘†β€˜suc 𝑁)𝐴 ∈ V)
19 satffunlem2lem2.b . . . . . . . . . 10 𝐡 = {π‘Ž ∈ (𝑀 ↑m Ο‰) ∣ βˆ€π‘§ ∈ 𝑀 ({βŸ¨π‘–, π‘§βŸ©} βˆͺ (π‘Ž β†Ύ (Ο‰ βˆ– {𝑖}))) ∈ (2nd β€˜π‘’)}
2019, 14rabex2 5295 . . . . . . . . 9 𝐡 ∈ V
2120a1i 11 . . . . . . . 8 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜suc 𝑁)) ∧ 𝑖 ∈ Ο‰) β†’ 𝐡 ∈ V)
2221ralrimiva 3140 . . . . . . 7 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜suc 𝑁)) β†’ βˆ€π‘– ∈ Ο‰ 𝐡 ∈ V)
2318, 22jca 513 . . . . . 6 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜suc 𝑁)) β†’ (βˆ€π‘£ ∈ (π‘†β€˜suc 𝑁)𝐴 ∈ V ∧ βˆ€π‘– ∈ Ο‰ 𝐡 ∈ V))
2423ralrimiva 3140 . . . . 5 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ βˆ€π‘’ ∈ (π‘†β€˜suc 𝑁)(βˆ€π‘£ ∈ (π‘†β€˜suc 𝑁)𝐴 ∈ V ∧ βˆ€π‘– ∈ Ο‰ 𝐡 ∈ V))
25 simplr 768 . . . . . . 7 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š))
266ancri 551 . . . . . . . 8 (𝑁 ∈ Ο‰ β†’ (suc 𝑁 ∈ Ο‰ ∧ 𝑁 ∈ Ο‰))
2726ad2antrr 725 . . . . . . 7 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (suc 𝑁 ∈ Ο‰ ∧ 𝑁 ∈ Ο‰))
2825, 27jca 513 . . . . . 6 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ (suc 𝑁 ∈ Ο‰ ∧ 𝑁 ∈ Ο‰)))
29 sssucid 6401 . . . . . 6 𝑁 βŠ† suc 𝑁
301satfsschain 34022 . . . . . 6 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ (suc 𝑁 ∈ Ο‰ ∧ 𝑁 ∈ Ο‰)) β†’ (𝑁 βŠ† suc 𝑁 β†’ (π‘†β€˜π‘) βŠ† (π‘†β€˜suc 𝑁)))
3128, 29, 30mpisyl 21 . . . . 5 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (π‘†β€˜π‘) βŠ† (π‘†β€˜suc 𝑁))
32 dmopab3rexdif 34063 . . . . 5 ((βˆ€π‘’ ∈ (π‘†β€˜suc 𝑁)(βˆ€π‘£ ∈ (π‘†β€˜suc 𝑁)𝐴 ∈ V ∧ βˆ€π‘– ∈ Ο‰ 𝐡 ∈ V) ∧ (π‘†β€˜π‘) βŠ† (π‘†β€˜suc 𝑁)) β†’ dom {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = 𝐡)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴))} = {π‘₯ ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))})
3324, 31, 32syl2anc 585 . . . 4 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ dom {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = 𝐡)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴))} = {π‘₯ ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))})
34 simpr 486 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘)))
35 fveqeq2 6855 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑒 β†’ ((1st β€˜π‘€) = (1st β€˜π‘’) ↔ (1st β€˜π‘’) = (1st β€˜π‘’)))
3635adantl 483 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) ∧ 𝑀 = 𝑒) β†’ ((1st β€˜π‘€) = (1st β€˜π‘’) ↔ (1st β€˜π‘’) = (1st β€˜π‘’)))
37 eqidd 2734 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ (1st β€˜π‘’) = (1st β€˜π‘’))
3834, 36, 37rspcedvd 3585 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ βˆƒπ‘€ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘€) = (1st β€˜π‘’))
392funeqi 6526 . . . . . . . . . . . . . . . . . . 19 (Fun (π‘†β€˜suc 𝑁) ↔ Fun ((𝑀 Sat 𝐸)β€˜suc 𝑁))
4039biimpi 215 . . . . . . . . . . . . . . . . . 18 (Fun (π‘†β€˜suc 𝑁) β†’ Fun ((𝑀 Sat 𝐸)β€˜suc 𝑁))
4140adantl 483 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ Fun ((𝑀 Sat 𝐸)β€˜suc 𝑁))
421fveq1i 6847 . . . . . . . . . . . . . . . . . 18 (π‘†β€˜π‘) = ((𝑀 Sat 𝐸)β€˜π‘)
4331, 42, 23sstr3g 3992 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁))
4441, 43jca 513 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (Fun ((𝑀 Sat 𝐸)β€˜suc 𝑁) ∧ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁)))
4544adantr 482 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ (Fun ((𝑀 Sat 𝐸)β€˜suc 𝑁) ∧ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁)))
46 funeldmdif 7984 . . . . . . . . . . . . . . 15 ((Fun ((𝑀 Sat 𝐸)β€˜suc 𝑁) ∧ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁)) β†’ ((1st β€˜π‘’) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)) ↔ βˆƒπ‘€ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘€) = (1st β€˜π‘’)))
4745, 46syl 17 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ ((1st β€˜π‘’) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)) ↔ βˆƒπ‘€ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘€) = (1st β€˜π‘’)))
4838, 47mpbird 257 . . . . . . . . . . . . 13 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ (1st β€˜π‘’) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)))
4948ex 414 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘)) β†’ (1st β€˜π‘’) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘))))
502, 42difeq12i 4084 . . . . . . . . . . . . . 14 ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘)) = (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))
5150eleq2i 2826 . . . . . . . . . . . . 13 (𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘)) ↔ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘)))
5251a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘)) ↔ 𝑒 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))))
5311eqcomd 2739 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (Fmlaβ€˜suc 𝑁) = dom ((𝑀 Sat 𝐸)β€˜suc 𝑁))
54 simpl 484 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ 𝑁 ∈ Ο‰)
554, 5, 543jca 1129 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ 𝑁 ∈ Ο‰))
56 satfdmfmla 34058 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ 𝑁 ∈ Ο‰) β†’ dom ((𝑀 Sat 𝐸)β€˜π‘) = (Fmlaβ€˜π‘))
5755, 56syl 17 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ dom ((𝑀 Sat 𝐸)β€˜π‘) = (Fmlaβ€˜π‘))
5857eqcomd 2739 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ (Fmlaβ€˜π‘) = dom ((𝑀 Sat 𝐸)β€˜π‘))
5958adantr 482 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (Fmlaβ€˜π‘) = dom ((𝑀 Sat 𝐸)β€˜π‘))
6053, 59difeq12d 4087 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) = (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)))
6160eleq2d 2820 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((1st β€˜π‘’) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ↔ (1st β€˜π‘’) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘))))
6249, 52, 613imtr4d 294 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘)) β†’ (1st β€˜π‘’) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
6362imp 408 . . . . . . . . . 10 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) β†’ (1st β€˜π‘’) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
6463adantr 482 . . . . . . . . 9 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ (1st β€˜π‘’) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
65 oveq1 7368 . . . . . . . . . . . . 13 (𝑓 = (1st β€˜π‘’) β†’ (π‘“βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”π‘”))
6665eqeq2d 2744 . . . . . . . . . . . 12 (𝑓 = (1st β€˜π‘’) β†’ (π‘₯ = (π‘“βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
6766rexbidv 3172 . . . . . . . . . . 11 (𝑓 = (1st β€˜π‘’) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
68 eqidd 2734 . . . . . . . . . . . . . 14 (𝑓 = (1st β€˜π‘’) β†’ 𝑖 = 𝑖)
69 id 22 . . . . . . . . . . . . . 14 (𝑓 = (1st β€˜π‘’) β†’ 𝑓 = (1st β€˜π‘’))
7068, 69goaleq12d 34009 . . . . . . . . . . . . 13 (𝑓 = (1st β€˜π‘’) β†’ βˆ€π‘”π‘–π‘“ = βˆ€π‘”π‘–(1st β€˜π‘’))
7170eqeq2d 2744 . . . . . . . . . . . 12 (𝑓 = (1st β€˜π‘’) β†’ (π‘₯ = βˆ€π‘”π‘–π‘“ ↔ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
7271rexbidv 3172 . . . . . . . . . . 11 (𝑓 = (1st β€˜π‘’) β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“ ↔ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
7367, 72orbi12d 918 . . . . . . . . . 10 (𝑓 = (1st β€˜π‘’) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
7473adantl 483 . . . . . . . . 9 ((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) ∧ 𝑓 = (1st β€˜π‘’)) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
754adantr 482 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ 𝑀 ∈ 𝑉)
765adantr 482 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ 𝐸 ∈ π‘Š)
776ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ suc 𝑁 ∈ Ο‰)
7875, 76, 773jca 1129 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ suc 𝑁 ∈ Ο‰))
79 satfrel 34025 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ suc 𝑁 ∈ Ο‰) β†’ Rel ((𝑀 Sat 𝐸)β€˜suc 𝑁))
8078, 79syl 17 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ Rel ((𝑀 Sat 𝐸)β€˜suc 𝑁))
812releqi 5737 . . . . . . . . . . . . . . . . 17 (Rel (π‘†β€˜suc 𝑁) ↔ Rel ((𝑀 Sat 𝐸)β€˜suc 𝑁))
8280, 81sylibr 233 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ Rel (π‘†β€˜suc 𝑁))
83 1stdm 7976 . . . . . . . . . . . . . . . 16 ((Rel (π‘†β€˜suc 𝑁) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) β†’ (1st β€˜π‘£) ∈ dom (π‘†β€˜suc 𝑁))
8482, 83sylan 581 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) β†’ (1st β€˜π‘£) ∈ dom (π‘†β€˜suc 𝑁))
8512eqcomd 2739 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (Fmlaβ€˜suc 𝑁) = dom (π‘†β€˜suc 𝑁))
8685adantr 482 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) β†’ (Fmlaβ€˜suc 𝑁) = dom (π‘†β€˜suc 𝑁))
8784, 86eleqtrrd 2837 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) β†’ (1st β€˜π‘£) ∈ (Fmlaβ€˜suc 𝑁))
8887ad4ant13 750 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ (1st β€˜π‘£) ∈ (Fmlaβ€˜suc 𝑁))
89 oveq2 7369 . . . . . . . . . . . . . . 15 (𝑔 = (1st β€˜π‘£) β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
9089eqeq2d 2744 . . . . . . . . . . . . . 14 (𝑔 = (1st β€˜π‘£) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
9190adantl 483 . . . . . . . . . . . . 13 (((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) ∧ 𝑔 = (1st β€˜π‘£)) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
92 simpr 486 . . . . . . . . . . . . 13 ((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
9388, 91, 92rspcedvd 3585 . . . . . . . . . . . 12 ((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ 𝑣 ∈ (π‘†β€˜suc 𝑁)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”))
9493rexlimdva2 3151 . . . . . . . . . . 11 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) β†’ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) β†’ βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
9594orim1d 965 . . . . . . . . . 10 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) β†’ ((βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
9695imp 408 . . . . . . . . 9 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))
9764, 74, 96rspcedvd 3585 . . . . . . . 8 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))) β†’ βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“))
9897rexlimdva2 3151 . . . . . . 7 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
9955adantr 482 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ 𝑁 ∈ Ο‰))
100 satfrel 34025 . . . . . . . . . . . . . 14 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ 𝑁 ∈ Ο‰) β†’ Rel ((𝑀 Sat 𝐸)β€˜π‘))
10199, 100syl 17 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ Rel ((𝑀 Sat 𝐸)β€˜π‘))
10242releqi 5737 . . . . . . . . . . . . 13 (Rel (π‘†β€˜π‘) ↔ Rel ((𝑀 Sat 𝐸)β€˜π‘))
103101, 102sylibr 233 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ Rel (π‘†β€˜π‘))
104 1stdm 7976 . . . . . . . . . . . 12 ((Rel (π‘†β€˜π‘) ∧ 𝑒 ∈ (π‘†β€˜π‘)) β†’ (1st β€˜π‘’) ∈ dom (π‘†β€˜π‘))
105103, 104sylan 581 . . . . . . . . . . 11 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) β†’ (1st β€˜π‘’) ∈ dom (π‘†β€˜π‘))
10642dmeqi 5864 . . . . . . . . . . . . . 14 dom (π‘†β€˜π‘) = dom ((𝑀 Sat 𝐸)β€˜π‘)
10799, 56syl 17 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ dom ((𝑀 Sat 𝐸)β€˜π‘) = (Fmlaβ€˜π‘))
108106, 107eqtrid 2785 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ dom (π‘†β€˜π‘) = (Fmlaβ€˜π‘))
109108eqcomd 2739 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (Fmlaβ€˜π‘) = dom (π‘†β€˜π‘))
110109adantr 482 . . . . . . . . . . 11 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) β†’ (Fmlaβ€˜π‘) = dom (π‘†β€˜π‘))
111105, 110eleqtrrd 2837 . . . . . . . . . 10 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) β†’ (1st β€˜π‘’) ∈ (Fmlaβ€˜π‘))
112111adantr 482 . . . . . . . . 9 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ (1st β€˜π‘’) ∈ (Fmlaβ€˜π‘))
11366rexbidv 3172 . . . . . . . . . 10 (𝑓 = (1st β€˜π‘’) β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
114113adantl 483 . . . . . . . . 9 ((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) ∧ 𝑓 = (1st β€˜π‘’)) β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
115 simpr 486 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘)))
116 fveqeq2 6855 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑣 β†’ ((1st β€˜π‘‘) = (1st β€˜π‘£) ↔ (1st β€˜π‘£) = (1st β€˜π‘£)))
117116adantl 483 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) ∧ 𝑑 = 𝑣) β†’ ((1st β€˜π‘‘) = (1st β€˜π‘£) ↔ (1st β€˜π‘£) = (1st β€˜π‘£)))
118 eqidd 2734 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ (1st β€˜π‘£) = (1st β€˜π‘£))
119115, 117, 118rspcedvd 3585 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ βˆƒπ‘‘ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘‘) = (1st β€˜π‘£))
12044adantr 482 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ (Fun ((𝑀 Sat 𝐸)β€˜suc 𝑁) ∧ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁)))
121 funeldmdif 7984 . . . . . . . . . . . . . . . . . 18 ((Fun ((𝑀 Sat 𝐸)β€˜suc 𝑁) ∧ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁)) β†’ ((1st β€˜π‘£) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)) ↔ βˆƒπ‘‘ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘‘) = (1st β€˜π‘£)))
122120, 121syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ ((1st β€˜π‘£) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)) ↔ βˆƒπ‘‘ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘‘) = (1st β€˜π‘£)))
123119, 122mpbird 257 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))) β†’ (1st β€˜π‘£) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)))
124123ex 414 . . . . . . . . . . . . . . 15 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘)) β†’ (1st β€˜π‘£) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘))))
12550eleq2i 2826 . . . . . . . . . . . . . . . 16 (𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘)))
126125a1i 11 . . . . . . . . . . . . . . 15 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))))
12710eqcomd 2739 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ (Fmlaβ€˜suc 𝑁) = dom ((𝑀 Sat 𝐸)β€˜suc 𝑁))
128127, 58difeq12d 4087 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) = (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)))
129128eleq2d 2820 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ ((1st β€˜π‘£) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ↔ (1st β€˜π‘£) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘))))
130129adantr 482 . . . . . . . . . . . . . . 15 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((1st β€˜π‘£) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ↔ (1st β€˜π‘£) ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘))))
131124, 126, 1303imtr4d 294 . . . . . . . . . . . . . 14 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘)) β†’ (1st β€˜π‘£) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
132131adantr 482 . . . . . . . . . . . . 13 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) β†’ (𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘)) β†’ (1st β€˜π‘£) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))))
133132imp 408 . . . . . . . . . . . 12 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ 𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) β†’ (1st β€˜π‘£) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
134133adantr 482 . . . . . . . . . . 11 ((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ 𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ (1st β€˜π‘£) ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)))
13590adantl 483 . . . . . . . . . . 11 (((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ 𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) ∧ 𝑔 = (1st β€˜π‘£)) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
136 simpr 486 . . . . . . . . . . 11 ((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ 𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
137134, 135, 136rspcedvd 3585 . . . . . . . . . 10 ((((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ 𝑣 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”))
138137r19.29an 3152 . . . . . . . . 9 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”))
139112, 114, 138rspcedvd 3585 . . . . . . . 8 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ (π‘†β€˜π‘)) ∧ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”))
140139rexlimdva2 3151 . . . . . . 7 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) β†’ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)))
14198, 140orim12d 964 . . . . . 6 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) β†’ (βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ∨ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”))))
1428adantr 482 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ suc 𝑁 ∈ Ο‰))
1439eqcomd 2739 . . . . . . . . . . . . 13 ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š ∧ suc 𝑁 ∈ Ο‰) β†’ (Fmlaβ€˜suc 𝑁) = dom ((𝑀 Sat 𝐸)β€˜suc 𝑁))
144142, 143syl 17 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (Fmlaβ€˜suc 𝑁) = dom ((𝑀 Sat 𝐸)β€˜suc 𝑁))
145107eqcomd 2739 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (Fmlaβ€˜π‘) = dom ((𝑀 Sat 𝐸)β€˜π‘))
146144, 145difeq12d 4087 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) = (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)))
147146eleq2d 2820 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑓 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ↔ 𝑓 ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘))))
148 eqid 2733 . . . . . . . . . . . . 13 (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
149148satfsschain 34022 . . . . . . . . . . . 12 (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š) ∧ (suc 𝑁 ∈ Ο‰ ∧ 𝑁 ∈ Ο‰)) β†’ (𝑁 βŠ† suc 𝑁 β†’ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁)))
15028, 29, 149mpisyl 21 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁))
151 releldmdifi 7981 . . . . . . . . . . 11 ((Rel ((𝑀 Sat 𝐸)β€˜suc 𝑁) ∧ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁)) β†’ (𝑓 ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)) β†’ βˆƒπ‘’ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘’) = 𝑓))
15280, 150, 151syl2anc 585 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑓 ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)) β†’ βˆƒπ‘’ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘’) = 𝑓))
153147, 152sylbid 239 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑓 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆƒπ‘’ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘’) = 𝑓))
15450eqcomi 2742 . . . . . . . . . . 11 (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘)) = ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))
155154rexeqi 3311 . . . . . . . . . 10 (βˆƒπ‘’ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘’) = 𝑓 ↔ βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(1st β€˜π‘’) = 𝑓)
156 r19.41v 3182 . . . . . . . . . . . 12 (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) ↔ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
157 oveq1 7368 . . . . . . . . . . . . . . . . . . 19 ((1st β€˜π‘’) = 𝑓 β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = (π‘“βŠΌπ‘”π‘”))
158157eqeq2d 2744 . . . . . . . . . . . . . . . . . 18 ((1st β€˜π‘’) = 𝑓 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = (π‘“βŠΌπ‘”π‘”)))
159158rexbidv 3172 . . . . . . . . . . . . . . . . 17 ((1st β€˜π‘’) = 𝑓 β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”)))
160 eqidd 2734 . . . . . . . . . . . . . . . . . . . 20 ((1st β€˜π‘’) = 𝑓 β†’ 𝑖 = 𝑖)
161 id 22 . . . . . . . . . . . . . . . . . . . 20 ((1st β€˜π‘’) = 𝑓 β†’ (1st β€˜π‘’) = 𝑓)
162160, 161goaleq12d 34009 . . . . . . . . . . . . . . . . . . 19 ((1st β€˜π‘’) = 𝑓 β†’ βˆ€π‘”π‘–(1st β€˜π‘’) = βˆ€π‘”π‘–π‘“)
163162eqeq2d 2744 . . . . . . . . . . . . . . . . . 18 ((1st β€˜π‘’) = 𝑓 β†’ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ↔ π‘₯ = βˆ€π‘”π‘–π‘“))
164163rexbidv 3172 . . . . . . . . . . . . . . . . 17 ((1st β€˜π‘’) = 𝑓 β†’ (βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ↔ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“))
165159, 164orbi12d 918 . . . . . . . . . . . . . . . 16 ((1st β€˜π‘’) = 𝑓 β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
166165adantl 483 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ↔ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)))
167142, 9syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) = (Fmlaβ€˜suc 𝑁))
168167eqcomd 2739 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (Fmlaβ€˜suc 𝑁) = dom ((𝑀 Sat 𝐸)β€˜suc 𝑁))
169168eleq2d 2820 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑔 ∈ (Fmlaβ€˜suc 𝑁) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜suc 𝑁)))
170 releldm2 7979 . . . . . . . . . . . . . . . . . . . . 21 (Rel ((𝑀 Sat 𝐸)β€˜suc 𝑁) β†’ (𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)(1st β€˜π‘£) = 𝑔))
17180, 170syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑔 ∈ dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)(1st β€˜π‘£) = 𝑔))
172169, 171bitrd 279 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑔 ∈ (Fmlaβ€˜suc 𝑁) ↔ βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)(1st β€˜π‘£) = 𝑔))
173 r19.41v 3182 . . . . . . . . . . . . . . . . . . . . 21 (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) ↔ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)(1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
1741eqcomi 2742 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 Sat 𝐸) = 𝑆
175174fveq1i 6847 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 Sat 𝐸)β€˜suc 𝑁) = (π‘†β€˜suc 𝑁)
176175rexeqi 3311 . . . . . . . . . . . . . . . . . . . . . 22 (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) ↔ βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)))
17789eqcoms 2741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1st β€˜π‘£) = 𝑔 β†’ ((1st β€˜π‘’)βŠΌπ‘”π‘”) = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
178177eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st β€˜π‘£) = 𝑔 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
179178biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
181180reximdv 3164 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
182176, 181biimtrid 241 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)((1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
183173, 182biimtrrid 242 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)(1st β€˜π‘£) = 𝑔 ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
184183expd 417 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘£ ∈ ((𝑀 Sat 𝐸)β€˜suc 𝑁)(1st β€˜π‘£) = 𝑔 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
185172, 184sylbid 239 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑔 ∈ (Fmlaβ€˜suc 𝑁) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
186185rexlimdv 3147 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
187186ad2antrr 725 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ (1st β€˜π‘’) = 𝑓) β†’ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
188187orim1d 965 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) β†’ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
189166, 188sylbird 260 . . . . . . . . . . . . . 14 (((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) ∧ (1st β€˜π‘’) = 𝑓) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
190189expimpd 455 . . . . . . . . . . . . 13 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ 𝑒 ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))) β†’ (((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ (βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
191190reximdva 3162 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))((1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
192156, 191biimtrrid 242 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(1st β€˜π‘’) = 𝑓 ∧ (βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“)) β†’ βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
193192expd 417 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(1st β€˜π‘’) = 𝑓 β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))))
194155, 193biimtrid 241 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘’ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘’) = 𝑓 β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))))
195153, 194syld 47 . . . . . . . 8 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑓 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ ((βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)))))
196195rexlimdv 3147 . . . . . . 7 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) β†’ βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’))))
197145eleq2d 2820 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑓 ∈ (Fmlaβ€˜π‘) ↔ 𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜π‘)))
19855, 100syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) β†’ Rel ((𝑀 Sat 𝐸)β€˜π‘))
199198adantr 482 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ Rel ((𝑀 Sat 𝐸)β€˜π‘))
200 releldm2 7979 . . . . . . . . . . 11 (Rel ((𝑀 Sat 𝐸)β€˜π‘) β†’ (𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜π‘) ↔ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)(1st β€˜π‘’) = 𝑓))
201199, 200syl 17 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑓 ∈ dom ((𝑀 Sat 𝐸)β€˜π‘) ↔ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)(1st β€˜π‘’) = 𝑓))
202197, 201bitrd 279 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑓 ∈ (Fmlaβ€˜π‘) ↔ βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)(1st β€˜π‘’) = 𝑓))
203 r19.41v 3182 . . . . . . . . . . 11 (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)((1st β€˜π‘’) = 𝑓 ∧ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)) ↔ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)(1st β€˜π‘’) = 𝑓 ∧ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)))
20442eqcomi 2742 . . . . . . . . . . . . 13 ((𝑀 Sat 𝐸)β€˜π‘) = (π‘†β€˜π‘)
205204rexeqi 3311 . . . . . . . . . . . 12 (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)((1st β€˜π‘’) = 𝑓 ∧ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)) ↔ βˆƒπ‘’ ∈ (π‘†β€˜π‘)((1st β€˜π‘’) = 𝑓 ∧ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)))
206158rexbidv 3172 . . . . . . . . . . . . . . . 16 ((1st β€˜π‘’) = 𝑓 β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)))
207206adantl 483 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ (1st β€˜π‘’) = 𝑓) β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) ↔ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)))
208146eleq2d 2820 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑔 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) ↔ 𝑔 ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘))))
209 releldmdifi 7981 . . . . . . . . . . . . . . . . . . . 20 ((Rel ((𝑀 Sat 𝐸)β€˜suc 𝑁) ∧ ((𝑀 Sat 𝐸)β€˜π‘) βŠ† ((𝑀 Sat 𝐸)β€˜suc 𝑁)) β†’ (𝑔 ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)) β†’ βˆƒπ‘£ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘£) = 𝑔))
21080, 150, 209syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑔 ∈ (dom ((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– dom ((𝑀 Sat 𝐸)β€˜π‘)) β†’ βˆƒπ‘£ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘£) = 𝑔))
211208, 210sylbid 239 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑔 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ βˆƒπ‘£ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘£) = 𝑔))
212154rexeqi 3311 . . . . . . . . . . . . . . . . . . 19 (βˆƒπ‘£ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘£) = 𝑔 ↔ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(1st β€˜π‘£) = 𝑔)
213178biimpcd 249 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ ((1st β€˜π‘£) = 𝑔 β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
214213adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ ((1st β€˜π‘£) = 𝑔 β†’ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
215214reximdv 3164 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”)) β†’ (βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(1st β€˜π‘£) = 𝑔 β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
216215ex 414 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ (βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(1st β€˜π‘£) = 𝑔 β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
217216com23 86 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(1st β€˜π‘£) = 𝑔 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
218212, 217biimtrid 241 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘£ ∈ (((𝑀 Sat 𝐸)β€˜suc 𝑁) βˆ– ((𝑀 Sat 𝐸)β€˜π‘))(1st β€˜π‘£) = 𝑔 β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
219211, 218syld 47 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑔 ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘)) β†’ (π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
220219rexlimdv 3147 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
221220adantr 482 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ (1st β€˜π‘’) = 𝑓) β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
222207, 221sylbird 260 . . . . . . . . . . . . . 14 ((((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) ∧ (1st β€˜π‘’) = 𝑓) β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”) β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
223222expimpd 455 . . . . . . . . . . . . 13 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (((1st β€˜π‘’) = 𝑓 ∧ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)) β†’ βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
224223reximdv 3164 . . . . . . . . . . . 12 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘’ ∈ (π‘†β€˜π‘)((1st β€˜π‘’) = 𝑓 ∧ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)) β†’ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
225205, 224biimtrid 241 . . . . . . . . . . 11 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)((1st β€˜π‘’) = 𝑓 ∧ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)) β†’ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
226203, 225biimtrrid 242 . . . . . . . . . 10 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)(1st β€˜π‘’) = 𝑓 ∧ βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)) β†’ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
227226expd 417 . . . . . . . . 9 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘’ ∈ ((𝑀 Sat 𝐸)β€˜π‘)(1st β€˜π‘’) = 𝑓 β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”) β†’ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
228202, 227sylbid 239 . . . . . . . 8 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (𝑓 ∈ (Fmlaβ€˜π‘) β†’ (βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”) β†’ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
229228rexlimdv 3147 . . . . . . 7 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”) β†’ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))))
230196, 229orim12d 964 . . . . . 6 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ∨ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”)) β†’ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))))
231141, 230impbid 211 . . . . 5 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£))) ↔ (βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ∨ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”))))
232231abbidv 2802 . . . 4 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ {π‘₯ ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)))} = {π‘₯ ∣ (βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ∨ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”))})
23333, 232eqtrd 2773 . . 3 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ dom {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = 𝐡)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴))} = {π‘₯ ∣ (βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ∨ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”))})
23412, 233ineq12d 4177 . 2 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (dom (π‘†β€˜suc 𝑁) ∩ dom {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = 𝐡)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴))}) = ((Fmlaβ€˜suc 𝑁) ∩ {π‘₯ ∣ (βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ∨ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”))}))
235 fmlasucdisj 34057 . . 3 (𝑁 ∈ Ο‰ β†’ ((Fmlaβ€˜suc 𝑁) ∩ {π‘₯ ∣ (βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ∨ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”))}) = βˆ…)
236235ad2antrr 725 . 2 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ ((Fmlaβ€˜suc 𝑁) ∩ {π‘₯ ∣ (βˆƒπ‘“ ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))(βˆƒπ‘” ∈ (Fmlaβ€˜suc 𝑁)π‘₯ = (π‘“βŠΌπ‘”π‘”) ∨ βˆƒπ‘– ∈ Ο‰ π‘₯ = βˆ€π‘”π‘–π‘“) ∨ βˆƒπ‘“ ∈ (Fmlaβ€˜π‘)βˆƒπ‘” ∈ ((Fmlaβ€˜suc 𝑁) βˆ– (Fmlaβ€˜π‘))π‘₯ = (π‘“βŠΌπ‘”π‘”))}) = βˆ…)
237234, 236eqtrd 2773 1 (((𝑁 ∈ Ο‰ ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ π‘Š)) ∧ Fun (π‘†β€˜suc 𝑁)) β†’ (dom (π‘†β€˜suc 𝑁) ∩ dom {⟨π‘₯, π‘¦βŸ© ∣ (βˆƒπ‘’ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(βˆƒπ‘£ ∈ (π‘†β€˜suc 𝑁)(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴) ∨ βˆƒπ‘– ∈ Ο‰ (π‘₯ = βˆ€π‘”π‘–(1st β€˜π‘’) ∧ 𝑦 = 𝐡)) ∨ βˆƒπ‘’ ∈ (π‘†β€˜π‘)βˆƒπ‘£ ∈ ((π‘†β€˜suc 𝑁) βˆ– (π‘†β€˜π‘))(π‘₯ = ((1st β€˜π‘’)βŠΌπ‘”(1st β€˜π‘£)) ∧ 𝑦 = 𝐴))}) = βˆ…)
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   βŠ† wss 3914  βˆ…c0 4286  {csn 4590  βŸ¨cop 4596  {copab 5171  dom cdm 5637   β†Ύ cres 5639  Rel wrel 5642  suc csuc 6323  Fun wfun 6494  β€˜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-nel 3047  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:  satffunlem2  34066
  Copyright terms: Public domain W3C validator