satffunlem1lem2 - Mathbox for Mario Carneiro

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

Theorem satffunlem1lem2 34389

Description: Lemma 2 for satffunlem1 34393. (Contributed by AV, 23-Oct-2023.)

**Assertion**
Ref	Expression
satffunlem1lem2	⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ((𝑀 Sat 𝐸)‘∅) ∩ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))}) = ∅)

Distinct variable groups: 𝑓,𝐸,𝑖,𝑢,𝑣,𝑥,𝑦 𝑓,𝑀,𝑖,𝑢,𝑣,𝑥,𝑦 𝑓,𝑉,𝑖,𝑢,𝑣,𝑥 𝑓,𝑊,𝑖,𝑢,𝑣,𝑥 𝑥,𝑗,𝑦 Allowed substitution hints: 𝐸(𝑗) 𝑀(𝑗) 𝑉(𝑦,𝑗) 𝑊(𝑦,𝑗)

Proof of Theorem satffunlem1lem2 Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano1 7878	. . . 4 ⊢ ∅ ∈ ω
2		satfdmfmla 34386	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω) → dom ((𝑀 Sat 𝐸)‘∅) = (Fmla‘∅))
3	1, 2	mp3an3 1450	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom ((𝑀 Sat 𝐸)‘∅) = (Fmla‘∅))
4		ovex 7441	. . . . . . . . . 10 ⊢ (𝑀 ↑_m ω) ∈ V
5	4	difexi 5328	. . . . . . . . 9 ⊢ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V
6	5	a1i 11	. . . . . . . 8 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V)
7	6	ralrimiva 3146	. . . . . . 7 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → ∀𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V)
8	4	rabex 5332	. . . . . . . . 9 ⊢ {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ V
9	8	a1i 11	. . . . . . . 8 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑖 ∈ ω) → {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ V)
10	9	ralrimiva 3146	. . . . . . 7 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → ∀𝑖 ∈ ω {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ V)
11	7, 10	jca 512	. . . . . 6 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → (∀𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V ∧ ∀𝑖 ∈ ω {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ V))
12	11	ralrimiva 3146	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ∀𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∀𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V ∧ ∀𝑖 ∈ ω {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ V))
13		dmopab2rex 5917	. . . . 5 ⊢ (∀𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∀𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V ∧ ∀𝑖 ∈ ω {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ V) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} = {𝑥 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))})
14	12, 13	syl 17	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} = {𝑥 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))})
15		satfrel 34353	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω) → Rel ((𝑀 Sat 𝐸)‘∅))
16	1, 15	mp3an3 1450	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Rel ((𝑀 Sat 𝐸)‘∅))
17		1stdm 8025	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑀 Sat 𝐸)‘∅) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → (1^st ‘𝑢) ∈ dom ((𝑀 Sat 𝐸)‘∅))
18	16, 17	sylan 580	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → (1^st ‘𝑢) ∈ dom ((𝑀 Sat 𝐸)‘∅))
19	2	eqcomd 2738	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω) → (Fmla‘∅) = dom ((𝑀 Sat 𝐸)‘∅))
20	1, 19	mp3an3 1450	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (Fmla‘∅) = dom ((𝑀 Sat 𝐸)‘∅))
21	20	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → (Fmla‘∅) = dom ((𝑀 Sat 𝐸)‘∅))
22	18, 21	eleqtrrd 2836	. . . . . . . . . 10 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → (1^st ‘𝑢) ∈ (Fmla‘∅))
23	22	adantr 481	. . . . . . . . 9 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (1^st ‘𝑢) ∈ (Fmla‘∅))
24		oveq1 7415	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑓⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔𝑔))
25	24	eqeq2d 2743	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = (𝑓⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
26	25	rexbidv 3178	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
27		eqidd 2733	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (1^st ‘𝑢) → 𝑖 = 𝑖)
28		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (1^st ‘𝑢) → 𝑓 = (1^st ‘𝑢))
29	27, 28	goaleq12d 34337	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → ∀_𝑔𝑖𝑓 = ∀_𝑔𝑖(1^st ‘𝑢))
30	29	eqeq2d 2743	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑖𝑓 ↔ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
31	30	rexbidv 3178	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓 ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
32	26, 31	orbi12d 917	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → ((∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
33	32	adantl 482	. . . . . . . . 9 ⊢ (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) ∧ 𝑓 = (1^st ‘𝑢)) → ((∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
34		1stdm 8025	. . . . . . . . . . . . . . . . 17 ⊢ ((Rel ((𝑀 Sat 𝐸)‘∅) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) → (1^st ‘𝑣) ∈ dom ((𝑀 Sat 𝐸)‘∅))
35	16, 34	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) → (1^st ‘𝑣) ∈ dom ((𝑀 Sat 𝐸)‘∅))
36	20	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) → (Fmla‘∅) = dom ((𝑀 Sat 𝐸)‘∅))
37	35, 36	eleqtrrd 2836	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) → (1^st ‘𝑣) ∈ (Fmla‘∅))
38	37	ad4ant13 749	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ (Fmla‘∅))
39		oveq2 7416	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (1^st ‘𝑣) → ((1^st ‘𝑢)⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
40	39	eqeq2d 2743	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (1^st ‘𝑣) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
41	40	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
42		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
43	38, 41, 42	rspcedvd 3614	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
44	43	ex 413	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
45	44	rexlimdva 3155	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
46	45	orim1d 964	. . . . . . . . . 10 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
47	46	imp 407	. . . . . . . . 9 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
48	23, 33, 47	rspcedvd 3614	. . . . . . . 8 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → ∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
49	48	ex 413	. . . . . . 7 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
50	49	rexlimdva 3155	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
51		releldm2 8028	. . . . . . . . . 10 ⊢ (Rel ((𝑀 Sat 𝐸)‘∅) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘∅) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑢) = 𝑓))
52	16, 51	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘∅) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑢) = 𝑓))
53	3	eleq2d 2819	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘∅) ↔ 𝑓 ∈ (Fmla‘∅)))
54	52, 53	bitr3d 280	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑢) = 𝑓 ↔ 𝑓 ∈ (Fmla‘∅)))
55		r19.41v 3188	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) ↔ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
56		oveq1 7415	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → ((1^st ‘𝑢)⊼_𝑔𝑔) = (𝑓⊼_𝑔𝑔))
57	56	eqeq2d 2743	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = (𝑓⊼_𝑔𝑔)))
58	57	rexbidv 3178	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔)))
59		eqidd 2733	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → 𝑖 = 𝑖)
60		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (1^st ‘𝑢) = 𝑓)
61	59, 60	goaleq12d 34337	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑖𝑓)
62	61	eqeq2d 2743	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ 𝑥 = ∀_𝑔𝑖𝑓))
63	62	rexbidv 3178	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
64	58, 63	orbi12d 917	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
65	64	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
66	3	eqcomd 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (Fmla‘∅) = dom ((𝑀 Sat 𝐸)‘∅))
67	66	eleq2d 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑔 ∈ (Fmla‘∅) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)‘∅)))
68		releldm2 8028	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel ((𝑀 Sat 𝐸)‘∅) → (𝑔 ∈ dom ((𝑀 Sat 𝐸)‘∅) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑣) = 𝑔))
69	16, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑔 ∈ dom ((𝑀 Sat 𝐸)‘∅) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑣) = 𝑔))
70	67, 69	bitrd 278	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑔 ∈ (Fmla‘∅) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑣) = 𝑔))
71		r19.41v 3188	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
72	39	eqcoms 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘𝑣) = 𝑔 → ((1^st ‘𝑢)⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
73	72	eqeq2d 2743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
74	73	biimpa 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
76	75	reximdv 3170	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
77	71, 76	biimtrrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
78	77	expd 416	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
79	70, 78	sylbid 239	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑔 ∈ (Fmla‘∅) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
80	79	rexlimdv 3153	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
81	80	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → (∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
82	81	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
83	82	orim1d 964	. . . . . . . . . . . . 13 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
84	65, 83	sylbird 259	. . . . . . . . . . . 12 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
85	84	expimpd 454	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)) → (((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
86	85	reximdva 3168	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
87	55, 86	biimtrrid 242	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
88	87	expd 416	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
89	54, 88	sylbird 259	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑓 ∈ (Fmla‘∅) → ((∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
90	89	rexlimdv 3153	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
91	50, 90	impbid 211	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ ∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
92	91	abbidv 2801	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → {𝑥 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))} = {𝑥 ∣ ∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)})
93	14, 92	eqtrd 2772	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} = {𝑥 ∣ ∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)})
94	3, 93	ineq12d 4213	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ((𝑀 Sat 𝐸)‘∅) ∩ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))}) = ((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)}))
95		fmla0disjsuc 34384	. 2 ⊢ ((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑓 ∈ (Fmla‘∅)(∃𝑔 ∈ (Fmla‘∅)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)}) = ∅
96	94, 95	eqtrdi 2788	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ((𝑀 Sat 𝐸)‘∅) ∩ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))}) = ∅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 {cab 2709 ∀wral 3061 ∃wrex 3070 {crab 3432 Vcvv 3474 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ∅c0 4322 {csn 4628 ⟨cop 4634 {copab 5210 dom cdm 5676 ↾ cres 5678 Rel wrel 5681 ‘cfv 6543 (class class class)co 7408 ωcom 7854 1^st c1st 7972 2^nd c2nd 7973 ↑_m cmap 8819 ⊼_𝑔cgna 34320 ∀_𝑔cgol 34321 Sat csat 34322 Fmlacfmla 34323

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7724 ax-inf2 9635

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7855 df-1st 7974 df-2nd 7975 df-frecs 8265 df-wrecs 8296 df-recs 8370 df-rdg 8409 df-1o 8465 df-2o 8466 df-map 8821 df-goel 34326 df-gona 34327 df-goal 34328 df-sat 34329 df-fmla 34331

This theorem is referenced by: satffunlem1 34393

W3C validator