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 34000

Description: Lemma 2 for satffunlem2 34002. (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 6843	. . . . 5 ⊢ (𝑆‘suc 𝑁) = ((𝑀 Sat 𝐸)‘suc 𝑁)
3	2	dmeqi 5860	. . . 4 ⊢ dom (𝑆‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)
4		simprl 769	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑀 ∈ 𝑉)
5		simprr 771	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝐸 ∈ 𝑊)
6		peano2 7827	. . . . . . . 8 ⊢ (𝑁 ∈ ω → suc 𝑁 ∈ ω)
7	6	adantr 481	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → suc 𝑁 ∈ ω)
8	4, 5, 7	3jca 1128	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
9		satfdmfmla 33994	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
10	8, 9	syl 17	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
11	10	adantr 481	. . . 4 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
12	3, 11	eqtrid 2788	. . 3 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom (𝑆‘suc 𝑁) = (Fmla‘suc 𝑁))
13		satffunlem2lem2.a	. . . . . . . . . 10 ⊢ 𝐴 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
14		ovex 7390	. . . . . . . . . . 11 ⊢ (𝑀 ↑_m ω) ∈ V
15	14	difexi 5285	. . . . . . . . . 10 ⊢ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V
16	13, 15	eqeltri 2834	. . . . . . . . 9 ⊢ 𝐴 ∈ V
17	16	a1i 11	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → 𝐴 ∈ V)
18	17	ralrimiva 3143	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V)
19		satffunlem2lem2.b	. . . . . . . . . 10 ⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}
20	19, 14	rabex2 5291	. . . . . . . . 9 ⊢ 𝐵 ∈ V
21	20	a1i 11	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑖 ∈ ω) → 𝐵 ∈ V)
22	21	ralrimiva 3143	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑖 ∈ ω 𝐵 ∈ V)
23	18, 22	jca 512	. . . . . 6 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → (∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V))
24	23	ralrimiva 3143	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ∀𝑢 ∈ (𝑆‘suc 𝑁)(∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V))
25		simplr 767	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊))
26	6	ancri 550	. . . . . . . 8 ⊢ (𝑁 ∈ ω → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
27	26	ad2antrr 724	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
28	25, 27	jca 512	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)))
29		sssucid 6397	. . . . . 6 ⊢ 𝑁 ⊆ suc 𝑁
30	1	satfsschain 33958	. . . . . 6 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)))
31	28, 29, 30	mpisyl 21	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁))
32		dmopab3rexdif 33999	. . . . 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 584	. . . 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 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
35		fveqeq2 6851	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑢 → ((1^st ‘𝑤) = (1^st ‘𝑢) ↔ (1^st ‘𝑢) = (1^st ‘𝑢)))
36	35	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) ∧ 𝑤 = 𝑢) → ((1^st ‘𝑤) = (1^st ‘𝑢) ↔ (1^st ‘𝑢) = (1^st ‘𝑢)))
37		eqidd 2737	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑢) = (1^st ‘𝑢))
38	34, 36, 37	rspcedvd 3583	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑤) = (1^st ‘𝑢))
39	2	funeqi 6522	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun (𝑆‘suc 𝑁) ↔ Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
40	39	biimpi 215	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝑆‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
41	40	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
42	1	fveq1i 6843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆‘𝑁) = ((𝑀 Sat 𝐸)‘𝑁)
43	31, 42, 2	3sstr3g 3988	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
44	41, 43	jca 512	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
45	44	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
46		funeldmdif 7980	. . . . . . . . . . . . . . 15 ⊢ ((Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → ((1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑤) = (1^st ‘𝑢)))
47	45, 46	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ((1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑤) = (1^st ‘𝑢)))
48	38, 47	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
49	48	ex 413	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
50	2, 42	difeq12i 4080	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) = (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))
51	50	eleq2i 2829	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
52	51	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))))
53	11	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
54		simpl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑁 ∈ ω)
55	4, 5, 54	3jca 1128	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω))
56		satfdmfmla 33994	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
57	55, 56	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
58	57	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
59	58	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
60	53, 59	difeq12d 4083	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
61	60	eleq2d 2823	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
62	49, 52, 61	3imtr4d 293	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
63	62	imp 407	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
64	63	adantr 481	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
65		oveq1 7364	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑓⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔𝑔))
66	65	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = (𝑓⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
67	66	rexbidv 3175	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
68		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (1^st ‘𝑢) → 𝑖 = 𝑖)
69		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (1^st ‘𝑢) → 𝑓 = (1^st ‘𝑢))
70	68, 69	goaleq12d 33945	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → ∀_𝑔𝑖𝑓 = ∀_𝑔𝑖(1^st ‘𝑢))
71	70	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑖𝑓 ↔ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
72	71	rexbidv 3175	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓 ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
73	67, 72	orbi12d 917	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
74	73	adantl 482	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) ∧ 𝑓 = (1^st ‘𝑢)) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
75	4	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝑀 ∈ 𝑉)
76	5	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝐸 ∈ 𝑊)
77	6	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → suc 𝑁 ∈ ω)
78	75, 76, 77	3jca 1128	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
79		satfrel 33961	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
80	78, 79	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
81	2	releqi 5733	. . . . . . . . . . . . . . . . 17 ⊢ (Rel (𝑆‘suc 𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
82	80, 81	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘suc 𝑁))
83		1stdm 7972	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ dom (𝑆‘suc 𝑁))
84	82, 83	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ dom (𝑆‘suc 𝑁))
85	12	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁))
86	85	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁))
87	84, 86	eleqtrrd 2841	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ (Fmla‘suc 𝑁))
88	87	ad4ant13 749	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ (Fmla‘suc 𝑁))
89		oveq2 7365	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (1^st ‘𝑣) → ((1^st ‘𝑢)⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
90	89	eqeq2d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (1^st ‘𝑣) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
91	90	adantl 482	. . . . . . . . . . . . 13 ⊢ (((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
92		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
93	88, 91, 92	rspcedvd 3583	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
94	93	rexlimdva2 3154	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
95	94	orim1d 964	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
96	95	imp 407	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
97	64, 74, 96	rspcedvd 3583	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
98	97	rexlimdva2 3154	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
99	55	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω))
100		satfrel 33961	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑁))
101	99, 100	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
102	42	releqi 5733	. . . . . . . . . . . . 13 ⊢ (Rel (𝑆‘𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘𝑁))
103	101, 102	sylibr 233	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘𝑁))
104		1stdm 7972	. . . . . . . . . . . 12 ⊢ ((Rel (𝑆‘𝑁) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ dom (𝑆‘𝑁))
105	103, 104	sylan 580	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ dom (𝑆‘𝑁))
106	42	dmeqi 5860	. . . . . . . . . . . . . 14 ⊢ dom (𝑆‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁)
107	99, 56	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
108	106, 107	eqtrid 2788	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom (𝑆‘𝑁) = (Fmla‘𝑁))
109	108	eqcomd 2742	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁))
110	109	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁))
111	105, 110	eleqtrrd 2841	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ (Fmla‘𝑁))
112	111	adantr 481	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑢) ∈ (Fmla‘𝑁))
113	66	rexbidv 3175	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
114	113	adantl 482	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑓 = (1^st ‘𝑢)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
115		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
116		fveqeq2 6851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑣 → ((1^st ‘𝑡) = (1^st ‘𝑣) ↔ (1^st ‘𝑣) = (1^st ‘𝑣)))
117	116	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) ∧ 𝑡 = 𝑣) → ((1^st ‘𝑡) = (1^st ‘𝑣) ↔ (1^st ‘𝑣) = (1^st ‘𝑣)))
118		eqidd 2737	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑣) = (1^st ‘𝑣))
119	115, 117, 118	rspcedvd 3583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑡) = (1^st ‘𝑣))
120	44	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
121		funeldmdif 7980	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → ((1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑡) = (1^st ‘𝑣)))
122	120, 121	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ((1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑡) = (1^st ‘𝑣)))
123	119, 122	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
124	123	ex 413	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
125	50	eleq2i 2829	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
126	125	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))))
127	10	eqcomd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
128	127, 58	difeq12d 4083	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
129	128	eleq2d 2823	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
130	129	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
131	124, 126, 130	3imtr4d 293	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
132	131	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
133	132	imp 407	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
134	133	adantr 481	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
135	90	adantl 482	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
136		simpr 485	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
137	134, 135, 136	rspcedvd 3583	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
138	137	r19.29an 3155	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
139	112, 114, 138	rspcedvd 3583	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))
140	139	rexlimdva2 3154	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
141	98, 140	orim12d 963	. . . . . 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‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))))
142	8	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
143	9	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
144	142, 143	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
145	107	eqcomd 2742	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
146	144, 145	difeq12d 4083	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
147	146	eleq2d 2823	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
148		eqid 2736	. . . . . . . . . . . . 13 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
149	148	satfsschain 33958	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
150	28, 29, 149	mpisyl 21	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
151		releldmdifi 7977	. . . . . . . . . . 11 ⊢ ((Rel ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → (𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓))
152	80, 150, 151	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓))
153	147, 152	sylbid 239	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓))
154	50	eqcomi 2745	. . . . . . . . . . 11 ⊢ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) = ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))
155	154	rexeqi 3312	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓 ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓)
156		r19.41v 3185	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
157		oveq1 7364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢) = 𝑓 → ((1^st ‘𝑢)⊼_𝑔𝑔) = (𝑓⊼_𝑔𝑔))
158	157	eqeq2d 2747	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = (𝑓⊼_𝑔𝑔)))
159	158	rexbidv 3175	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔)))
160		eqidd 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑢) = 𝑓 → 𝑖 = 𝑖)
161		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑢) = 𝑓 → (1^st ‘𝑢) = 𝑓)
162	160, 161	goaleq12d 33945	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢) = 𝑓 → ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑖𝑓)
163	162	eqeq2d 2747	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ 𝑥 = ∀_𝑔𝑖𝑓))
164	163	rexbidv 3175	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
165	159, 164	orbi12d 917	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
166	165	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
167	142, 9	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
168	167	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁))
169	168	eleq2d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁)))
170		releldm2 7975	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Rel ((𝑀 Sat 𝐸)‘suc 𝑁) → (𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔))
171	80, 170	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔))
172	169, 171	bitrd 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔))
173		r19.41v 3185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
174	1	eqcomi 2745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 Sat 𝐸) = 𝑆
175	174	fveq1i 6843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 Sat 𝐸)‘suc 𝑁) = (𝑆‘suc 𝑁)
176	175	rexeqi 3312	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
177	89	eqcoms 2744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1^st ‘𝑣) = 𝑔 → ((1^st ‘𝑢)⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
178	177	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
179	178	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
180	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
181	180	reximdv 3167	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
182	176, 181	biimtrid 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
183	173, 182	biimtrrid 242	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
184	183	expd 416	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
185	172, 184	sylbid 239	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
186	185	rexlimdv 3150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
187	186	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
188	187	orim1d 964	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
189	166, 188	sylbird 259	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
190	189	expimpd 454	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
191	190	reximdva 3165	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
192	156, 191	biimtrrid 242	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
193	192	expd 416	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
194	155, 193	biimtrid 241	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
195	153, 194	syld 47	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
196	195	rexlimdv 3150	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
197	145	eleq2d 2823	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁)))
198	55, 100	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
199	198	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
200		releldm2 7975	. . . . . . . . . . 11 ⊢ (Rel ((𝑀 Sat 𝐸)‘𝑁) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓))
201	199, 200	syl 17	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓))
202	197, 201	bitrd 278	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓))
203		r19.41v 3185	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) ↔ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
204	42	eqcomi 2745	. . . . . . . . . . . . 13 ⊢ ((𝑀 Sat 𝐸)‘𝑁) = (𝑆‘𝑁)
205	204	rexeqi 3312	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) ↔ ∃𝑢 ∈ (𝑆‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
206	158	rexbidv 3175	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
207	206	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
208	146	eleq2d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
209		releldmdifi 7977	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Rel ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → (𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔))
210	80, 150, 209	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔))
211	208, 210	sylbid 239	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔))
212	154	rexeqi 3312	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔 ↔ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔)
213	178	biimpcd 248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ((1^st ‘𝑣) = 𝑔 → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
214	213	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ((1^st ‘𝑣) = 𝑔 → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
215	214	reximdv 3167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔 → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
216	215	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔 → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
217	216	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
218	212, 217	biimtrid 241	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
219	211, 218	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
220	219	rexlimdv 3150	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
221	220	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
222	207, 221	sylbird 259	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
223	222	expimpd 454	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
224	223	reximdv 3167	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
225	205, 224	biimtrid 241	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
226	203, 225	biimtrrid 242	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
227	226	expd 416	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
228	202, 227	sylbid 239	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
229	228	rexlimdv 3150	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
230	196, 229	orim12d 963	. . . . . 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 ‘𝑣)))))
231	141, 230	impbid 211	. . . . 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‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))))
232	231	abbidv 2805	. . . 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‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))})
233	33, 232	eqtrd 2776	. . 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‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))})
234	12, 233	ineq12d 4173	. 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‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}))
235		fmlasucdisj 33993	. . 3 ⊢ (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}) = ∅)
236	235	ad2antrr 724	. 2 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}) = ∅)
237	234, 236	eqtrd 2776	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 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 {cab 2713 ∀wral 3064 ∃wrex 3073 {crab 3407 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 {csn 4586 ⟨cop 4592 {copab 5167 dom cdm 5633 ↾ cres 5635 Rel wrel 5638 suc csuc 6319 Fun wfun 6490 ‘cfv 6496 (class class class)co 7357 ωcom 7802 1^st c1st 7919 2^nd c2nd 7920 ↑_m cmap 8765 ⊼_𝑔cgna 33928 ∀_𝑔cgol 33929 Sat csat 33930 Fmlacfmla 33931

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 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577

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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-map 8767 df-goel 33934 df-gona 33935 df-goal 33936 df-sat 33937 df-fmla 33939

This theorem is referenced by: satffunlem2 34002

W3C validator