satffunlem2lem2 - Mathbox for Mario Carneiro

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

Theorem satffunlem2lem2 36140

Description: Lemma 2 for satffunlem2 36142. (Contributed by AV, 27-Oct-2023.)

**Hypotheses**
Ref	Expression
satffunlem2lem2.s	⊢ 𝑆 = (𝑀 Sat 𝐸)
satffunlem2lem2.a	⊢ 𝐴 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
satffunlem2lem2.b	⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}

**Assertion**
Ref	Expression
satffunlem2lem2	⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (dom (𝑆‘suc 𝑁) ∩ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))}) = ∅)

Distinct variable groups: 𝐴,𝑖,𝑥,𝑦 𝑥,𝐵,𝑦 𝑖,𝐸,𝑢,𝑣,𝑥 𝑀,𝑎 𝑖,𝑀,𝑢,𝑣,𝑥 𝑖,𝑁,𝑢,𝑣,𝑥,𝑦 𝑆,𝑖,𝑢,𝑣,𝑥,𝑦 𝑖,𝑉,𝑢,𝑣,𝑥 𝑖,𝑊,𝑢,𝑣,𝑥 Allowed substitution hints: 𝐴(𝑧, 𝑣, 𝑢, 𝑎) 𝐵(𝑧, 𝑣, 𝑢, 𝑖, 𝑎) 𝑆(𝑧, 𝑎) 𝐸(𝑦, 𝑧, 𝑎) 𝑀(𝑦, 𝑧) 𝑁(𝑧, 𝑎) 𝑉(𝑦, 𝑧, 𝑎) 𝑊(𝑦, 𝑧, 𝑎)

Proof of Theorem satffunlem2lem2 Dummy variables 𝑓 𝑔 𝑡 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		satffunlem2lem2.s	. . . . . 6 ⊢ 𝑆 = (𝑀 Sat 𝐸)
2	1	fveq1i 6878	. . . . 5 ⊢ (𝑆‘suc 𝑁) = ((𝑀 Sat 𝐸)‘suc 𝑁)
3	2	dmeqi 5886	. . . 4 ⊢ dom (𝑆‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)
4		simprl 783	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑀 ∈ 𝑉)
5		simprr 785	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝐸 ∈ 𝑊)
6		peano2 7890	. . . . . . . 8 ⊢ (𝑁 ∈ ω → suc 𝑁 ∈ ω)
7	6	adantr 486	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → suc 𝑁 ∈ ω)
8	4, 5, 7	3jca 1146	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
9		satfdmfmla 36134	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
10	8, 9	syl 18	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
11	10	adantr 486	. . . 4 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
12	3, 11	eqtrid 2808	. . 3 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom (𝑆‘suc 𝑁) = (Fmla‘suc 𝑁))
13		satffunlem2lem2.a	. . . . . . . . . 10 ⊢ 𝐴 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
14		ovex 7445	. . . . . . . . . . 11 ⊢ (𝑀 ↑_m ω) ∈ V
15	14	difexi 5292	. . . . . . . . . 10 ⊢ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V
16	13, 15	eqeltri 2857	. . . . . . . . 9 ⊢ 𝐴 ∈ V
17	16	a1i 11	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → 𝐴 ∈ V)
18	17	ralrimiva 3155	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V)
19		satffunlem2lem2.b	. . . . . . . . . 10 ⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}
20	19, 14	rabex2 5302	. . . . . . . . 9 ⊢ 𝐵 ∈ V
21	20	a1i 11	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑖 ∈ ω) → 𝐵 ∈ V)
22	21	ralrimiva 3155	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑖 ∈ ω 𝐵 ∈ V)
23	18, 22	jca 521	. . . . . 6 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → (∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V))
24	23	ralrimiva 3155	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ∀𝑢 ∈ (𝑆‘suc 𝑁)(∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V))
25		simplr 781	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊))
26	6	ancri 559	. . . . . . . 8 ⊢ (𝑁 ∈ ω → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
27	26	ad2antrr 739	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
28	25, 27	jca 521	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)))
29		sssucid 6438	. . . . . 6 ⊢ 𝑁 ⊆ suc 𝑁
30	1	satfsschain 36098	. . . . . 6 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)))
31	28, 29, 30	mpisyl 22	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁))
32		dmopab3rexdif 36139	. . . . 5 ⊢ ((∀𝑢 ∈ (𝑆‘suc 𝑁)(∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))} = {𝑥 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))})
33	24, 31, 32	syl2anc 596	. . . 4 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))} = {𝑥 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))})
34		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
35		fveqeq2 6886	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑢 → ((1^st ‘𝑤) = (1^st ‘𝑢) ↔ (1^st ‘𝑢) = (1^st ‘𝑢)))
36	35	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) ∧ 𝑤 = 𝑢) → ((1^st ‘𝑤) = (1^st ‘𝑢) ↔ (1^st ‘𝑢) = (1^st ‘𝑢)))
37		eqidd 2762	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑢) = (1^st ‘𝑢))
38	34, 36, 37	rspcedvd 3579	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑤) = (1^st ‘𝑢))
39	2	funeqi 6552	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝑆‘suc 𝑁) ↔ Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
40	39	bilani 510	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
41	1	fveq1i 6878	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆‘𝑁) = ((𝑀 Sat 𝐸)‘𝑁)
42	31, 41, 2	3sstr3g 3983	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
43	40, 42	jca 521	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
44	43	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
45		funeldmdif 8048	. . . . . . . . . . . . . . 15 ⊢ ((Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → ((1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑤) = (1^st ‘𝑢)))
46	44, 45	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ((1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑤) = (1^st ‘𝑢)))
47	38, 46	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
48	47	ex 418	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
49	2, 41	difeq12i 4072	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) = (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))
50	49	eleq2i 2853	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
51	50	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))))
52	11	eqcomd 2767	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
53		simpl 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑁 ∈ ω)
54	4, 5, 53	3jca 1146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω))
55		satfdmfmla 36134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
56	54, 55	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
57	56	eqcomd 2767	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
58	57	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
59	52, 58	difeq12d 4075	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
60	59	eleq2d 2847	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
61	48, 51, 60	3imtr4d 297	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
62	61	imp 412	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
63	62	adantr 486	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
64		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑓⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔𝑔))
65	64	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = (𝑓⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
66	65	rexbidv 3187	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
67		eqidd 2762	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (1^st ‘𝑢) → 𝑖 = 𝑖)
68		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (1^st ‘𝑢) → 𝑓 = (1^st ‘𝑢))
69	67, 68	goaleq12d 36085	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → ∀_𝑔𝑖𝑓 = ∀_𝑔𝑖(1^st ‘𝑢))
70	69	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑖𝑓 ↔ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
71	70	rexbidv 3187	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓 ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
72	66, 71	orbi12d 932	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
73	72	adantl 487	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) ∧ 𝑓 = (1^st ‘𝑢)) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
74	4	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝑀 ∈ 𝑉)
75	5	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝐸 ∈ 𝑊)
76	6	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → suc 𝑁 ∈ ω)
77	74, 75, 76	3jca 1146	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
78		satfrel 36101	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
79	77, 78	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
80	2	releqi 5754	. . . . . . . . . . . . . . . . 17 ⊢ (Rel (𝑆‘suc 𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
81	79, 80	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘suc 𝑁))
82		1stdm 8040	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ dom (𝑆‘suc 𝑁))
83	81, 82	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ dom (𝑆‘suc 𝑁))
84	12	eqcomd 2767	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁))
85	84	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁))
86	83, 85	eleqtrrd 2864	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ (Fmla‘suc 𝑁))
87	86	ad4ant13 764	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ (Fmla‘suc 𝑁))
88		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (1^st ‘𝑣) → ((1^st ‘𝑢)⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
89	88	eqeq2d 2772	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (1^st ‘𝑣) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
90	89	adantl 487	. . . . . . . . . . . . 13 ⊢ (((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
91		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
92	87, 90, 91	rspcedvd 3579	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
93	92	rexlimdva2 3166	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
94	93	orim1d 981	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
95	94	imp 412	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
96	63, 73, 95	rspcedvd 3579	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
97	96	rexlimdva2 3166	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
98	54	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω))
99		satfrel 36101	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑁))
100	98, 99	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
101	41	releqi 5754	. . . . . . . . . . . . 13 ⊢ (Rel (𝑆‘𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘𝑁))
102	100, 101	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘𝑁))
103		1stdm 8040	. . . . . . . . . . . 12 ⊢ ((Rel (𝑆‘𝑁) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ dom (𝑆‘𝑁))
104	102, 103	sylan 592	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ dom (𝑆‘𝑁))
105	41	dmeqi 5886	. . . . . . . . . . . . . 14 ⊢ dom (𝑆‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁)
106	98, 55	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
107	105, 106	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom (𝑆‘𝑁) = (Fmla‘𝑁))
108	107	eqcomd 2767	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁))
109	108	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁))
110	104, 109	eleqtrrd 2864	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ (Fmla‘𝑁))
111	110	adantr 486	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑢) ∈ (Fmla‘𝑁))
112	65	rexbidv 3187	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
113	112	adantl 487	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑓 = (1^st ‘𝑢)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
114		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
115		fveqeq2 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑣 → ((1^st ‘𝑡) = (1^st ‘𝑣) ↔ (1^st ‘𝑣) = (1^st ‘𝑣)))
116	115	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) ∧ 𝑡 = 𝑣) → ((1^st ‘𝑡) = (1^st ‘𝑣) ↔ (1^st ‘𝑣) = (1^st ‘𝑣)))
117		eqidd 2762	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑣) = (1^st ‘𝑣))
118	114, 116, 117	rspcedvd 3579	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑡) = (1^st ‘𝑣))
119	43	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
120		funeldmdif 8048	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → ((1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑡) = (1^st ‘𝑣)))
121	119, 120	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ((1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑡) = (1^st ‘𝑣)))
122	118, 121	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
123	122	ex 418	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
124	49	eleq2i 2853	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
125	124	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))))
126	10	eqcomd 2767	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
127	126, 57	difeq12d 4075	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
128	127	eleq2d 2847	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
129	128	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
130	123, 125, 129	3imtr4d 297	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
131	130	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
132	131	imp 412	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
133	132	adantr 486	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
134	89	adantl 487	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
135		simpr 490	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
136	133, 134, 135	rspcedvd 3579	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
137	136	r19.29an 3167	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
138	111, 113, 137	rspcedvd 3579	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))
139	138	rexlimdva2 3166	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
140	97, 139	orim12d 979	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))))
141	8	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
142	9	eqcomd 2767	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
143	141, 142	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
144	106	eqcomd 2767	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
145	143, 144	difeq12d 4075	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
146	145	eleq2d 2847	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
147		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
148	147	satfsschain 36098	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
149	28, 29, 148	mpisyl 22	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
150		releldmdifi 8045	. . . . . . . . . . 11 ⊢ ((Rel ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → (𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓))
151	79, 149, 150	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓))
152	146, 151	sylbid 243	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓))
153	49	eqcomi 2770	. . . . . . . . . . 11 ⊢ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) = ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))
154	153	rexeqi 3319	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓 ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓)
155		r19.41v 3193	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
156		oveq1 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢) = 𝑓 → ((1^st ‘𝑢)⊼_𝑔𝑔) = (𝑓⊼_𝑔𝑔))
157	156	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = (𝑓⊼_𝑔𝑔)))
158	157	rexbidv 3187	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔)))
159		eqidd 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑢) = 𝑓 → 𝑖 = 𝑖)
160		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑢) = 𝑓 → (1^st ‘𝑢) = 𝑓)
161	159, 160	goaleq12d 36085	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢) = 𝑓 → ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑖𝑓)
162	161	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ 𝑥 = ∀_𝑔𝑖𝑓))
163	162	rexbidv 3187	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
164	158, 163	orbi12d 932	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
165	164	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
166	141, 9	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
167	166	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
168	167	eleq2d 2847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁)))
169		releldm2 8043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Rel ((𝑀 Sat 𝐸)‘suc 𝑁) → (𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔))
170	79, 169	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔))
171	168, 170	bitrd 282	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔))
172		r19.41v 3193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
173	1	eqcomi 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 Sat 𝐸) = 𝑆
174	173	fveq1i 6878	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 Sat 𝐸)‘suc 𝑁) = (𝑆‘suc 𝑁)
175	174	rexeqi 3319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
176	88	eqcoms 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1^st ‘𝑣) = 𝑔 → ((1^st ‘𝑢)⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
177	176	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
178	177	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
179	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
180	179	reximdv 3178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
181	175, 180	biimtrid 245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
182	172, 181	biimtrrid 246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
183	182	expd 421	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
184	171, 183	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
185	184	rexlimdv 3162	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
186	185	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
187	186	orim1d 981	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
188	165, 187	sylbird 263	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
189	188	expimpd 459	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
190	189	reximdva 3176	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
191	155, 190	biimtrrid 246	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
192	191	expd 421	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
193	154, 192	biimtrid 245	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
194	152, 193	syld 48	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
195	194	rexlimdv 3162	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
196	144	eleq2d 2847	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁)))
197	54, 99	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
198	197	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
199		releldm2 8043	. . . . . . . . . . 11 ⊢ (Rel ((𝑀 Sat 𝐸)‘𝑁) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓))
200	198, 199	syl 18	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓))
201	196, 200	bitrd 282	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓))
202		r19.41v 3193	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) ↔ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
203	41	eqcomi 2770	. . . . . . . . . . . . 13 ⊢ ((𝑀 Sat 𝐸)‘𝑁) = (𝑆‘𝑁)
204	203	rexeqi 3319	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) ↔ ∃𝑢 ∈ (𝑆‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
205	157	rexbidv 3187	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
206	205	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
207	145	eleq2d 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
208		releldmdifi 8045	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Rel ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → (𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔))
209	79, 149, 208	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔))
210	207, 209	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔))
211	153	rexeqi 3319	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔 ↔ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔)
212	177	biimpcd 252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ((1^st ‘𝑣) = 𝑔 → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
213	212	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ((1^st ‘𝑣) = 𝑔 → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
214	213	reximdv 3178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔 → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
215	214	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔 → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
216	215	com23 87	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
217	211, 216	biimtrid 245	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
218	210, 217	syld 48	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
219	218	rexlimdv 3162	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
220	219	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
221	206, 220	sylbird 263	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
222	221	expimpd 459	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
223	222	reximdv 3178	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
224	204, 223	biimtrid 245	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
225	202, 224	biimtrrid 246	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
226	225	expd 421	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
227	201, 226	sylbid 243	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
228	227	rexlimdv 3162	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
229	195, 228	orim12d 979	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
230	140, 229	impbid 215	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ↔ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))))
231	230	abbidv 2827	. . . 4 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → {𝑥 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))} = {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))})
232	33, 231	eqtrd 2796	. . 3 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))} = {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))})
233	12, 232	ineq12d 4167	. 2 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (dom (𝑆‘suc 𝑁) ∩ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))}) = ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}))
234		fmlasucdisj 36133	. . 3 ⊢ (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}) = ∅)
235	234	ad2antrr 739	. 2 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}) = ∅)
236	233, 235	eqtrd 2796	1 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (dom (𝑆‘suc 𝑁) ∩ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))}) = ∅)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 {cab 2739 ∀wral 3077 ∃wrex 3087 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 {csn 4584 ⟨cop 4590 {copab 5167 dom cdm 5651 ↾ cres 5653 Rel wrel 5656 suc csuc 6357 Fun wfun 6525 ‘cfv 6531 (class class class)co 7412 ωcom 7866 1^st c1st 7988 2^nd c2nd 7989 ↑_m cmap 8831 ⊼_𝑔cgna 36068 ∀_𝑔cgol 36069 Sat csat 36070 Fmlacfmla 36071

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-map 8833 df-goel 36074 df-gona 36075 df-goal 36076 df-sat 36077 df-fmla 36079

This theorem is used by: satffunlem2 36142

W3C validator