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 35793

Description: Lemma 2 for satffunlem2 35795. (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 6880	. . . . 5 ⊢ (𝑆‘suc 𝑁) = ((𝑀 Sat 𝐸)‘suc 𝑁)
3	2	dmeqi 5892	. . . 4 ⊢ dom (𝑆‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)
4		simprl 782	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑀 ∈ 𝑉)
5		simprr 784	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝐸 ∈ 𝑊)
6		peano2 7882	. . . . . . . 8 ⊢ (𝑁 ∈ ω → suc 𝑁 ∈ ω)
7	6	adantr 485	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → suc 𝑁 ∈ ω)
8	4, 5, 7	3jca 1144	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
9		satfdmfmla 35787	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
10	8, 9	syl 18	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
11	10	adantr 485	. . . 4 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
12	3, 11	eqtrid 2816	. . 3 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom (𝑆‘suc 𝑁) = (Fmla‘suc 𝑁))
13		satffunlem2lem2.a	. . . . . . . . . 10 ⊢ 𝐴 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
14		ovex 7441	. . . . . . . . . . 11 ⊢ (𝑀 ↑_m ω) ∈ V
15	14	difexi 5298	. . . . . . . . . 10 ⊢ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V
16	13, 15	eqeltri 2865	. . . . . . . . 9 ⊢ 𝐴 ∈ V
17	16	a1i 11	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → 𝐴 ∈ V)
18	17	ralrimiva 3163	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V)
19		satffunlem2lem2.b	. . . . . . . . . 10 ⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}
20	19, 14	rabex2 5309	. . . . . . . . 9 ⊢ 𝐵 ∈ V
21	20	a1i 11	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑖 ∈ ω) → 𝐵 ∈ V)
22	21	ralrimiva 3163	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑖 ∈ ω 𝐵 ∈ V)
23	18, 22	jca 520	. . . . . 6 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → (∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V))
24	23	ralrimiva 3163	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ∀𝑢 ∈ (𝑆‘suc 𝑁)(∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V))
25		simplr 780	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊))
26	6	ancri 558	. . . . . . . 8 ⊢ (𝑁 ∈ ω → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
27	26	ad2antrr 738	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
28	25, 27	jca 520	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)))
29		sssucid 6440	. . . . . 6 ⊢ 𝑁 ⊆ suc 𝑁
30	1	satfsschain 35751	. . . . . 6 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)))
31	28, 29, 30	mpisyl 22	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁))
32		dmopab3rexdif 35792	. . . . 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 595	. . . 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 489	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
35		fveqeq2 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑢 → ((1^st ‘𝑤) = (1^st ‘𝑢) ↔ (1^st ‘𝑢) = (1^st ‘𝑢)))
36	35	adantl 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) ∧ 𝑤 = 𝑢) → ((1^st ‘𝑤) = (1^st ‘𝑢) ↔ (1^st ‘𝑢) = (1^st ‘𝑢)))
37		eqidd 2770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑢) = (1^st ‘𝑢))
38	34, 36, 37	rspcedvd 3592	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑤) = (1^st ‘𝑢))
39	2	funeqi 6554	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝑆‘suc 𝑁) ↔ Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
40	39	bilani 509	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
41	1	fveq1i 6880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆‘𝑁) = ((𝑀 Sat 𝐸)‘𝑁)
42	31, 41, 2	3sstr3g 3997	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
43	40, 42	jca 520	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
44	43	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
45		funeldmdif 8041	. . . . . . . . . . . . . . 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 417	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
49	2, 41	difeq12i 4087	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) = (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))
50	49	eleq2i 2861	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
51	50	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))))
52	11	eqcomd 2775	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
53		simpl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑁 ∈ ω)
54	4, 5, 53	3jca 1144	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω))
55		satfdmfmla 35787	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
56	54, 55	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
57	56	eqcomd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
58	57	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
59	52, 58	difeq12d 4090	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
60	59	eleq2d 2855	. . . . . . . . . . . 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 411	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
63	62	adantr 485	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
64		oveq1 7415	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑓⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔𝑔))
65	64	eqeq2d 2780	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = (𝑓⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
66	65	rexbidv 3195	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
67		eqidd 2770	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (1^st ‘𝑢) → 𝑖 = 𝑖)
68		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (1^st ‘𝑢) → 𝑓 = (1^st ‘𝑢))
69	67, 68	goaleq12d 35738	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → ∀_𝑔𝑖𝑓 = ∀_𝑔𝑖(1^st ‘𝑢))
70	69	eqeq2d 2780	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑖𝑓 ↔ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
71	70	rexbidv 3195	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓 ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
72	66, 71	orbi12d 931	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
73	72	adantl 486	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) ∧ 𝑓 = (1^st ‘𝑢)) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
74	4	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝑀 ∈ 𝑉)
75	5	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝐸 ∈ 𝑊)
76	6	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → suc 𝑁 ∈ ω)
77	74, 75, 76	3jca 1144	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
78		satfrel 35754	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
79	77, 78	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
80	2	releqi 5762	. . . . . . . . . . . . . . . . 17 ⊢ (Rel (𝑆‘suc 𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
81	79, 80	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘suc 𝑁))
82		1stdm 8033	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ dom (𝑆‘suc 𝑁))
83	81, 82	sylan 591	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ dom (𝑆‘suc 𝑁))
84	12	eqcomd 2775	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁))
85	84	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁))
86	83, 85	eleqtrrd 2872	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ (Fmla‘suc 𝑁))
87	86	ad4ant13 763	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ (Fmla‘suc 𝑁))
88		oveq2 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (1^st ‘𝑣) → ((1^st ‘𝑢)⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
89	88	eqeq2d 2780	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (1^st ‘𝑣) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
90	89	adantl 486	. . . . . . . . . . . . 13 ⊢ (((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
91		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
92	87, 90, 91	rspcedvd 3592	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
93	92	rexlimdva2 3174	. . . . . . . . . . 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 411	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
96	63, 73, 95	rspcedvd 3592	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
97	96	rexlimdva2 3174	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
98	54	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω))
99		satfrel 35754	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑁))
100	98, 99	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
101	41	releqi 5762	. . . . . . . . . . . . 13 ⊢ (Rel (𝑆‘𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘𝑁))
102	100, 101	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘𝑁))
103		1stdm 8033	. . . . . . . . . . . 12 ⊢ ((Rel (𝑆‘𝑁) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ dom (𝑆‘𝑁))
104	102, 103	sylan 591	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ dom (𝑆‘𝑁))
105	41	dmeqi 5892	. . . . . . . . . . . . . 14 ⊢ dom (𝑆‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁)
106	98, 55	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
107	105, 106	eqtrid 2816	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom (𝑆‘𝑁) = (Fmla‘𝑁))
108	107	eqcomd 2775	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁))
109	108	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁))
110	104, 109	eleqtrrd 2872	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ (Fmla‘𝑁))
111	110	adantr 485	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑢) ∈ (Fmla‘𝑁))
112	65	rexbidv 3195	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
113	112	adantl 486	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑓 = (1^st ‘𝑢)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
114		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
115		fveqeq2 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑣 → ((1^st ‘𝑡) = (1^st ‘𝑣) ↔ (1^st ‘𝑣) = (1^st ‘𝑣)))
116	115	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) ∧ 𝑡 = 𝑣) → ((1^st ‘𝑡) = (1^st ‘𝑣) ↔ (1^st ‘𝑣) = (1^st ‘𝑣)))
117		eqidd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑣) = (1^st ‘𝑣))
118	114, 116, 117	rspcedvd 3592	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑡) = (1^st ‘𝑣))
119	43	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
120		funeldmdif 8041	. . . . . . . . . . . . . . . . . 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 417	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
124	49	eleq2i 2861	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
125	124	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))))
126	10	eqcomd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
127	126, 57	difeq12d 4090	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
128	127	eleq2d 2855	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
129	128	adantr 485	. . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
132	131	imp 411	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
133	132	adantr 485	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
134	89	adantl 486	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
135		simpr 489	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
136	133, 134, 135	rspcedvd 3592	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
137	136	r19.29an 3175	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
138	111, 113, 137	rspcedvd 3592	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))
139	138	rexlimdva2 3174	. . . . . . 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 485	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
142	9	eqcomd 2775	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
143	141, 142	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
144	106	eqcomd 2775	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
145	143, 144	difeq12d 4090	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
146	145	eleq2d 2855	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
147		eqid 2769	. . . . . . . . . . . . 13 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
148	147	satfsschain 35751	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
149	28, 29, 148	mpisyl 22	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
150		releldmdifi 8038	. . . . . . . . . . 11 ⊢ ((Rel ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → (𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓))
151	79, 149, 150	syl2anc 595	. . . . . . . . . 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 2778	. . . . . . . . . . 11 ⊢ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) = ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))
154	153	rexeqi 3328	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓 ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓)
155		r19.41v 3201	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
156		oveq1 7415	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢) = 𝑓 → ((1^st ‘𝑢)⊼_𝑔𝑔) = (𝑓⊼_𝑔𝑔))
157	156	eqeq2d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = (𝑓⊼_𝑔𝑔)))
158	157	rexbidv 3195	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔)))
159		eqidd 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑢) = 𝑓 → 𝑖 = 𝑖)
160		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑢) = 𝑓 → (1^st ‘𝑢) = 𝑓)
161	159, 160	goaleq12d 35738	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢) = 𝑓 → ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑖𝑓)
162	161	eqeq2d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ 𝑥 = ∀_𝑔𝑖𝑓))
163	162	rexbidv 3195	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
164	158, 163	orbi12d 931	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
165	164	adantl 486	. . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
168	167	eleq2d 2855	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁)))
169		releldm2 8036	. . . . . . . . . . . . . . . . . . . . 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 3201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
173	1	eqcomi 2778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 Sat 𝐸) = 𝑆
174	173	fveq1i 6880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 Sat 𝐸)‘suc 𝑁) = (𝑆‘suc 𝑁)
175	174	rexeqi 3328	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
176	88	eqcoms 2777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1^st ‘𝑣) = 𝑔 → ((1^st ‘𝑢)⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
177	176	eqeq2d 2780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
178	177	biimpa 481	. . . . . . . . . . . . . . . . . . . . . . . 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 3186	. . . . . . . . . . . . . . . . . . . . . 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 420	. . . . . . . . . . . . . . . . . . 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 3170	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
186	185	ad2antrr 738	. . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
190	189	reximdva 3184	. . . . . . . . . . . 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 420	. . . . . . . . . 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 3170	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
196	144	eleq2d 2855	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁)))
197	54, 99	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
198	197	adantr 485	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
199		releldm2 8036	. . . . . . . . . . 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 3201	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) ↔ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
203	41	eqcomi 2778	. . . . . . . . . . . . 13 ⊢ ((𝑀 Sat 𝐸)‘𝑁) = (𝑆‘𝑁)
204	203	rexeqi 3328	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) ↔ ∃𝑢 ∈ (𝑆‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
205	157	rexbidv 3195	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
206	205	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
207	145	eleq2d 2855	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
208		releldmdifi 8038	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Rel ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → (𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔))
209	79, 149, 208	syl2anc 595	. . . . . . . . . . . . . . . . . . 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 3328	. . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ((1^st ‘𝑣) = 𝑔 → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
214	213	reximdv 3186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔 → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
215	214	ex 417	. . . . . . . . . . . . . . . . . . . 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 3170	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
220	219	adantr 485	. . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
223	222	reximdv 3186	. . . . . . . . . . . 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 420	. . . . . . . . 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 3170	. . . . . . 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 2835	. . . 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 2804	. . 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 4182	. 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 35786	. . 3 ⊢ (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}) = ∅)
235	234	ad2antrr 738	. 2 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}) = ∅)
236	233, 235	eqtrd 2804	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

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 {cab 2747 ∀wral 3085 ∃wrex 3095 {crab 3423 Vcvv 3463 ∖ cdif 3910 ∪ cun 3911 ∩ cin 3912 ⊆ wss 3913 ∅c0 4294 {csn 4591 ⟨cop 4597 {copab 5174 dom cdm 5659 ↾ cres 5661 Rel wrel 5664 suc csuc 6359 Fun wfun 6527 ‘cfv 6533 (class class class)co 7408 ωcom 7858 1^st c1st 7980 2^nd c2nd 7981 ↑_m cmap 8820 ⊼_𝑔cgna 35721 ∀_𝑔cgol 35722 Sat csat 35723 Fmlacfmla 35724

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-inf2 9606

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-map 8822 df-goel 35727 df-gona 35728 df-goal 35729 df-sat 35730 df-fmla 35732

This theorem is referenced by: satffunlem2 35795

W3C validator