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 35412

Description: Lemma 2 for satffunlem2 35414. (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 6906	. . . . 5 ⊢ (𝑆‘suc 𝑁) = ((𝑀 Sat 𝐸)‘suc 𝑁)
3	2	dmeqi 5914	. . . 4 ⊢ dom (𝑆‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)
4		simprl 770	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑀 ∈ 𝑉)
5		simprr 772	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝐸 ∈ 𝑊)
6		peano2 7913	. . . . . . . 8 ⊢ (𝑁 ∈ ω → suc 𝑁 ∈ ω)
7	6	adantr 480	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → suc 𝑁 ∈ ω)
8	4, 5, 7	3jca 1128	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
9		satfdmfmla 35406	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
10	8, 9	syl 17	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁))
11	10	adantr 480	. . . 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 7465	. . . . . . . . . . 11 ⊢ (𝑀 ↑_m ω) ∈ V
15	14	difexi 5329	. . . . . . . . . 10 ⊢ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ V
16	13, 15	eqeltri 2836	. . . . . . . . 9 ⊢ 𝐴 ∈ V
17	16	a1i 11	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → 𝐴 ∈ V)
18	17	ralrimiva 3145	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V)
19		satffunlem2lem2.b	. . . . . . . . . 10 ⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}
20	19, 14	rabex2 5340	. . . . . . . . 9 ⊢ 𝐵 ∈ V
21	20	a1i 11	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑖 ∈ ω) → 𝐵 ∈ V)
22	21	ralrimiva 3145	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑖 ∈ ω 𝐵 ∈ V)
23	18, 22	jca 511	. . . . . 6 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → (∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V))
24	23	ralrimiva 3145	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ∀𝑢 ∈ (𝑆‘suc 𝑁)(∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V))
25		simplr 768	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊))
26	6	ancri 549	. . . . . . . 8 ⊢ (𝑁 ∈ ω → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
27	26	ad2antrr 726	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
28	25, 27	jca 511	. . . . . 6 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)))
29		sssucid 6463	. . . . . 6 ⊢ 𝑁 ⊆ suc 𝑁
30	1	satfsschain 35370	. . . . . 6 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)))
31	28, 29, 30	mpisyl 21	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁))
32		dmopab3rexdif 35411	. . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
35		fveqeq2 6914	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑢 → ((1^st ‘𝑤) = (1^st ‘𝑢) ↔ (1^st ‘𝑢) = (1^st ‘𝑢)))
36	35	adantl 481	. . . . . . . . . . . . . . 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 3623	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑤) = (1^st ‘𝑢))
39	2	funeqi 6586	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun (𝑆‘suc 𝑁) ↔ Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
40	39	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun (𝑆‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
41	40	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
42	1	fveq1i 6906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆‘𝑁) = ((𝑀 Sat 𝐸)‘𝑁)
43	31, 42, 2	3sstr3g 4035	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
44	41, 43	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
45	44	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
46		funeldmdif 8074	. . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
49	48	ex 412	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
50	2, 42	difeq12i 4123	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) = (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))
51	50	eleq2i 2832	. . . . . . . . . . . . 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 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑁 ∈ ω)
55	4, 5, 54	3jca 1128	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω))
56		satfdmfmla 35406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
57	55, 56	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁))
58	57	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
59	58	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁))
60	53, 59	difeq12d 4126	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
61	60	eleq2d 2826	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
62	49, 52, 61	3imtr4d 294	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
63	62	imp 406	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
64	63	adantr 480	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (1^st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
65		oveq1 7439	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑓⊼_𝑔𝑔) = ((1^st ‘𝑢)⊼_𝑔𝑔))
66	65	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = (𝑓⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
67	66	rexbidv 3178	. . . . . . . . . . 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 35357	. . . . . . . . . . . . 13 ⊢ (𝑓 = (1^st ‘𝑢) → ∀_𝑔𝑖𝑓 = ∀_𝑔𝑖(1^st ‘𝑢))
71	70	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑓 = (1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑖𝑓 ↔ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
72	71	rexbidv 3178	. . . . . . . . . . 11 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓 ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
73	67, 72	orbi12d 918	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
74	73	adantl 481	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) ∧ 𝑓 = (1^st ‘𝑢)) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
75	4	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝑀 ∈ 𝑉)
76	5	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝐸 ∈ 𝑊)
77	6	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → suc 𝑁 ∈ ω)
78	75, 76, 77	3jca 1128	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω))
79		satfrel 35373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
80	78, 79	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
81	2	releqi 5786	. . . . . . . . . . . . . . . . 17 ⊢ (Rel (𝑆‘suc 𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘suc 𝑁))
82	80, 81	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘suc 𝑁))
83		1stdm 8066	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁))
87	84, 86	eleqtrrd 2843	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1^st ‘𝑣) ∈ (Fmla‘suc 𝑁))
88	87	ad4ant13 751	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ (Fmla‘suc 𝑁))
89		oveq2 7440	. . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . 13 ⊢ (((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
92		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
93	88, 91, 92	rspcedvd 3623	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
94	93	rexlimdva2 3156	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
95	94	orim1d 967	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
96	95	imp 406	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))
97	64, 74, 96	rspcedvd 3623	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
98	97	rexlimdva2 3156	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
99	55	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω))
100		satfrel 35373	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑁))
101	99, 100	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
102	42	releqi 5786	. . . . . . . . . . . . 13 ⊢ (Rel (𝑆‘𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘𝑁))
103	101, 102	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘𝑁))
104		1stdm 8066	. . . . . . . . . . . 12 ⊢ ((Rel (𝑆‘𝑁) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ dom (𝑆‘𝑁))
105	103, 104	sylan 580	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ dom (𝑆‘𝑁))
106	42	dmeqi 5914	. . . . . . . . . . . . . 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 480	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁))
111	105, 110	eleqtrrd 2843	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1^st ‘𝑢) ∈ (Fmla‘𝑁))
112	111	adantr 480	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑢) ∈ (Fmla‘𝑁))
113	66	rexbidv 3178	. . . . . . . . . 10 ⊢ (𝑓 = (1^st ‘𝑢) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
114	113	adantl 481	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑓 = (1^st ‘𝑢)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
115		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))
116		fveqeq2 6914	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑣 → ((1^st ‘𝑡) = (1^st ‘𝑣) ↔ (1^st ‘𝑣) = (1^st ‘𝑣)))
117	116	adantl 481	. . . . . . . . . . . . . . . . . 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 3623	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑡) = (1^st ‘𝑣))
120	44	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
121		funeldmdif 8074	. . . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
124	123	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
125	50	eleq2i 2832	. . . . . . . . . . . . . . . 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 4126	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
129	128	eleq2d 2826	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
130	129	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1^st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
131	124, 126, 130	3imtr4d 294	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
132	131	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))))
133	132	imp 406	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
134	133	adantr 480	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → (1^st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))
135	90	adantl 481	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) ∧ 𝑔 = (1^st ‘𝑣)) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
136		simpr 484	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
137	134, 135, 136	rspcedvd 3623	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
138	137	r19.29an 3157	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔))
139	112, 114, 138	rspcedvd 3623	. . . . . . . 8 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))) → ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))
140	139	rexlimdva2 3156	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
141	98, 140	orim12d 966	. . . . . 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 480	. . . . . . . . . . . . 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 4126	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))
147	146	eleq2d 2826	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
148		eqid 2736	. . . . . . . . . . . . 13 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
149	148	satfsschain 35370	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
150	28, 29, 149	mpisyl 21	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
151		releldmdifi 8071	. . . . . . . . . . 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 240	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓))
154	50	eqcomi 2745	. . . . . . . . . . 11 ⊢ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) = ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))
155	154	rexeqi 3324	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑢) = 𝑓 ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓)
156		r19.41v 3188	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
157		oveq1 7439	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢) = 𝑓 → ((1^st ‘𝑢)⊼_𝑔𝑔) = (𝑓⊼_𝑔𝑔))
158	157	eqeq2d 2747	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ 𝑥 = (𝑓⊼_𝑔𝑔)))
159	158	rexbidv 3178	. . . . . . . . . . . . . . . . 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 35357	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑢) = 𝑓 → ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑖𝑓)
163	162	eqeq2d 2747	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑢) = 𝑓 → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ 𝑥 = ∀_𝑔𝑖𝑓))
164	163	rexbidv 3178	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓))
165	159, 164	orbi12d 918	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)))
166	165	adantl 481	. . . . . . . . . . . . . . 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 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁)))
170		releldm2 8069	. . . . . . . . . . . . . . . . . . . . 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 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔))
173		r19.41v 3188	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)))
174	1	eqcomi 2745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 Sat 𝐸) = 𝑆
175	174	fveq1i 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 Sat 𝐸)‘suc 𝑁) = (𝑆‘suc 𝑁)
176	175	rexeqi 3324	. . . . . . . . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . . . . . . . . . . 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 3169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
182	176, 181	biimtrid 242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
183	173, 182	biimtrrid 243	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
184	183	expd 415	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1^st ‘𝑣) = 𝑔 → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
185	172, 184	sylbid 240	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
186	185	rexlimdv 3152	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
187	186	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
188	187	orim1d 967	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
189	166, 188	sylbird 260	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1^st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
190	189	expimpd 453	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
191	190	reximdva 3167	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
192	156, 191	biimtrrid 243	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
193	192	expd 415	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
194	155, 193	biimtrid 242	. . . . . . . . 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 3152	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
197	145	eleq2d 2826	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁)))
198	55, 100	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
199	198	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁))
200		releldm2 8069	. . . . . . . . . . 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 279	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓))
203		r19.41v 3188	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) ↔ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
204	42	eqcomi 2745	. . . . . . . . . . . . 13 ⊢ ((𝑀 Sat 𝐸)‘𝑁) = (𝑆‘𝑁)
205	204	rexeqi 3324	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) ↔ ∃𝑢 ∈ (𝑆‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
206	158	rexbidv 3178	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
207	206	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)))
208	146	eleq2d 2826	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))))
209		releldmdifi 8071	. . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔))
212	154	rexeqi 3324	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1^st ‘𝑣) = 𝑔 ↔ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔)
213	178	biimpcd 249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ((1^st ‘𝑣) = 𝑔 → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
214	213	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → ((1^st ‘𝑣) = 𝑔 → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
215	214	reximdv 3169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1^st ‘𝑣) = 𝑔 → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
216	215	ex 412	. . . . . . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . . . . 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 3152	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
221	220	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
222	207, 221	sylbird 260	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1^st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
223	222	expimpd 453	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
224	223	reximdv 3169	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
225	205, 224	biimtrid 242	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
226	203, 225	biimtrrid 243	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
227	226	expd 415	. . . . . . . . 9 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1^st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
228	202, 227	sylbid 240	. . . . . . . 8 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))))
229	228	rexlimdv 3152	. . . . . . 7 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
230	196, 229	orim12d 966	. . . . . 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 212	. . . . 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 2807	. . . 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 4220	. 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 35405	. . 3 ⊢ (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼_𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼_𝑔𝑔))}) = ∅)
236	235	ad2antrr 726	. 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 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 {cab 2713 ∀wral 3060 ∃wrex 3069 {crab 3435 Vcvv 3479 ∖ cdif 3947 ∪ cun 3948 ∩ cin 3949 ⊆ wss 3950 ∅c0 4332 {csn 4625 ⟨cop 4631 {copab 5204 dom cdm 5684 ↾ cres 5686 Rel wrel 5689 suc csuc 6385 Fun wfun 6554 ‘cfv 6560 (class class class)co 7432 ωcom 7888 1^st c1st 8013 2^nd c2nd 8014 ↑_m cmap 8867 ⊼_𝑔cgna 35340 ∀_𝑔cgol 35341 Sat csat 35342 Fmlacfmla 35343

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-inf2 9682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-ov 7435 df-oprab 7436 df-mpo 7437 df-om 7889 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-map 8869 df-goel 35346 df-gona 35347 df-goal 35348 df-sat 35349 df-fmla 35351

This theorem is referenced by: satffunlem2 35414

W3C validator