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

Theorem satfdmlem 32850
 Description: Lemma for satfdm 32851. (Contributed by AV, 12-Oct-2023.)
Assertion
Ref Expression
satfdmlem (((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎))))
Distinct variable groups:   𝐸,𝑎,𝑏,𝑖,𝑢,𝑣   𝐹,𝑎,𝑏,𝑖,𝑢,𝑣   𝑀,𝑎,𝑏,𝑖,𝑢,𝑣   𝑁,𝑎,𝑏,𝑖,𝑢,𝑣   𝑉,𝑎,𝑏,𝑖,𝑢,𝑣   𝑊,𝑎,𝑏,𝑖,𝑢,𝑣   𝑌,𝑎,𝑏,𝑖,𝑢,𝑣   𝑥,𝑎,𝑏,𝑖,𝑢,𝑣
Allowed substitution hints:   𝐸(𝑥)   𝐹(𝑥)   𝑀(𝑥)   𝑁(𝑥)   𝑉(𝑥)   𝑊(𝑥)   𝑌(𝑥)

Proof of Theorem satfdmlem
Dummy variables 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 satfrel 32849 . . . . 5 ((𝑀𝑉𝐸𝑊𝑌 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑌))
21adantr 484 . . . 4 (((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) → Rel ((𝑀 Sat 𝐸)‘𝑌))
3 1stdm 7748 . . . 4 ((Rel ((𝑀 Sat 𝐸)‘𝑌) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (1st𝑢) ∈ dom ((𝑀 Sat 𝐸)‘𝑌))
42, 3sylan 583 . . 3 ((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (1st𝑢) ∈ dom ((𝑀 Sat 𝐸)‘𝑌))
5 eleq2 2840 . . . . . 6 (dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌) → ((1st𝑢) ∈ dom ((𝑀 Sat 𝐸)‘𝑌) ↔ (1st𝑢) ∈ dom ((𝑁 Sat 𝐹)‘𝑌)))
65adantl 485 . . . . 5 (((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) → ((1st𝑢) ∈ dom ((𝑀 Sat 𝐸)‘𝑌) ↔ (1st𝑢) ∈ dom ((𝑁 Sat 𝐹)‘𝑌)))
76adantr 484 . . . 4 ((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → ((1st𝑢) ∈ dom ((𝑀 Sat 𝐸)‘𝑌) ↔ (1st𝑢) ∈ dom ((𝑁 Sat 𝐹)‘𝑌)))
8 fvex 6675 . . . . . 6 (1st𝑢) ∈ V
9 eldm2g 5744 . . . . . 6 ((1st𝑢) ∈ V → ((1st𝑢) ∈ dom ((𝑁 Sat 𝐹)‘𝑌) ↔ ∃𝑠⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)))
108, 9ax-mp 5 . . . . 5 ((1st𝑢) ∈ dom ((𝑁 Sat 𝐹)‘𝑌) ↔ ∃𝑠⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌))
11 simpr 488 . . . . . . . 8 (((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) → ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌))
122ad4antr 731 . . . . . . . . . . . 12 (((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → Rel ((𝑀 Sat 𝐸)‘𝑌))
13 1stdm 7748 . . . . . . . . . . . 12 ((Rel ((𝑀 Sat 𝐸)‘𝑌) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (1st𝑣) ∈ dom ((𝑀 Sat 𝐸)‘𝑌))
1412, 13sylancom 591 . . . . . . . . . . 11 (((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (1st𝑣) ∈ dom ((𝑀 Sat 𝐸)‘𝑌))
15 eleq2 2840 . . . . . . . . . . . . 13 (dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌) → ((1st𝑣) ∈ dom ((𝑀 Sat 𝐸)‘𝑌) ↔ (1st𝑣) ∈ dom ((𝑁 Sat 𝐹)‘𝑌)))
1615ad5antlr 734 . . . . . . . . . . . 12 (((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → ((1st𝑣) ∈ dom ((𝑀 Sat 𝐸)‘𝑌) ↔ (1st𝑣) ∈ dom ((𝑁 Sat 𝐹)‘𝑌)))
17 fvex 6675 . . . . . . . . . . . . . 14 (1st𝑣) ∈ V
18 eldm2g 5744 . . . . . . . . . . . . . 14 ((1st𝑣) ∈ V → ((1st𝑣) ∈ dom ((𝑁 Sat 𝐹)‘𝑌) ↔ ∃𝑟⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)))
1917, 18ax-mp 5 . . . . . . . . . . . . 13 ((1st𝑣) ∈ dom ((𝑁 Sat 𝐹)‘𝑌) ↔ ∃𝑟⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌))
20 simpr 488 . . . . . . . . . . . . . . . 16 ((((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) → ⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌))
21 vex 3413 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 ∈ V
228, 21op1std 7708 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = ⟨(1st𝑢), 𝑠⟩ → (1st𝑎) = (1st𝑢))
2322eqcomd 2764 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ⟨(1st𝑢), 𝑠⟩ → (1st𝑢) = (1st𝑎))
2423ad3antlr 730 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) → (1st𝑢) = (1st𝑎))
25 vex 3413 . . . . . . . . . . . . . . . . . . . . 21 𝑟 ∈ V
2617, 25op1std 7708 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = ⟨(1st𝑣), 𝑟⟩ → (1st𝑏) = (1st𝑣))
2726eqcomd 2764 . . . . . . . . . . . . . . . . . . 19 (𝑏 = ⟨(1st𝑣), 𝑟⟩ → (1st𝑣) = (1st𝑏))
2824, 27oveqan12d 7174 . . . . . . . . . . . . . . . . . 18 (((((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑏 = ⟨(1st𝑣), 𝑟⟩) → ((1st𝑢)⊼𝑔(1st𝑣)) = ((1st𝑎)⊼𝑔(1st𝑏)))
2928eqeq2d 2769 . . . . . . . . . . . . . . . . 17 (((((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑏 = ⟨(1st𝑣), 𝑟⟩) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ↔ 𝑥 = ((1st𝑎)⊼𝑔(1st𝑏))))
3029biimpd 232 . . . . . . . . . . . . . . . 16 (((((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑏 = ⟨(1st𝑣), 𝑟⟩) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → 𝑥 = ((1st𝑎)⊼𝑔(1st𝑏))))
3120, 30rspcimedv 3534 . . . . . . . . . . . . . . 15 ((((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏))))
3231ex 416 . . . . . . . . . . . . . 14 (((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)))))
3332exlimdv 1934 . . . . . . . . . . . . 13 (((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (∃𝑟⟨(1st𝑣), 𝑟⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)))))
3419, 33syl5bi 245 . . . . . . . . . . . 12 (((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → ((1st𝑣) ∈ dom ((𝑁 Sat 𝐹)‘𝑌) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)))))
3516, 34sylbid 243 . . . . . . . . . . 11 (((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → ((1st𝑣) ∈ dom ((𝑀 Sat 𝐸)‘𝑌) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)))))
3614, 35mpd 15 . . . . . . . . . 10 (((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏))))
3736rexlimdva 3208 . . . . . . . . 9 ((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) → ∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏))))
38 eqidd 2759 . . . . . . . . . . . . . 14 (𝑎 = ⟨(1st𝑢), 𝑠⟩ → 𝑖 = 𝑖)
3938, 23goaleq12d 32833 . . . . . . . . . . . . 13 (𝑎 = ⟨(1st𝑢), 𝑠⟩ → ∀𝑔𝑖(1st𝑢) = ∀𝑔𝑖(1st𝑎))
4039eqeq2d 2769 . . . . . . . . . . . 12 (𝑎 = ⟨(1st𝑢), 𝑠⟩ → (𝑥 = ∀𝑔𝑖(1st𝑢) ↔ 𝑥 = ∀𝑔𝑖(1st𝑎)))
4140biimpd 232 . . . . . . . . . . 11 (𝑎 = ⟨(1st𝑢), 𝑠⟩ → (𝑥 = ∀𝑔𝑖(1st𝑢) → 𝑥 = ∀𝑔𝑖(1st𝑎)))
4241adantl 485 . . . . . . . . . 10 ((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) → (𝑥 = ∀𝑔𝑖(1st𝑢) → 𝑥 = ∀𝑔𝑖(1st𝑎)))
4342reximdv 3197 . . . . . . . . 9 ((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢) → ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎)))
4437, 43orim12d 962 . . . . . . . 8 ((((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑎 = ⟨(1st𝑢), 𝑠⟩) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → (∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎))))
4511, 44rspcimedv 3534 . . . . . . 7 (((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) ∧ ⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎))))
4645ex 416 . . . . . 6 ((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎)))))
4746exlimdv 1934 . . . . 5 ((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → (∃𝑠⟨(1st𝑢), 𝑠⟩ ∈ ((𝑁 Sat 𝐹)‘𝑌) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎)))))
4810, 47syl5bi 245 . . . 4 ((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → ((1st𝑢) ∈ dom ((𝑁 Sat 𝐹)‘𝑌) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎)))))
497, 48sylbid 243 . . 3 ((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → ((1st𝑢) ∈ dom ((𝑀 Sat 𝐸)‘𝑌) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎)))))
504, 49mpd 15 . 2 ((((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎))))
5150rexlimdva 3208 1 (((𝑀𝑉𝐸𝑊𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st𝑎)⊼𝑔(1st𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st𝑎))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃wrex 3071  Vcvv 3409  ⟨cop 4531  dom cdm 5527  Rel wrel 5532  ‘cfv 6339  (class class class)co 7155  ωcom 7584  1st c1st 7696  ⊼𝑔cgna 32816  ∀𝑔cgol 32817   Sat csat 32818 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-inf2 9142 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7585  df-1st 7698  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-goel 32822  df-goal 32824  df-sat 32825 This theorem is referenced by:  satfdm  32851
 Copyright terms: Public domain W3C validator