Theorem satfv0 36290

Description: The value of the satisfaction predicate as function over wff codes at ∅. (Contributed by AV, 8-Oct-2023.)

Hypothesis

Ref	Expression
satfv0.s	⊢ 𝑆 = (𝑀 Sat 𝐸)

Assertion

Ref	Expression
satfv0	⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})

Distinct variable groups:   𝐸,𝑎,𝑖,𝑗,𝑥,𝑦   𝑀,𝑎,𝑖,𝑗,𝑥,𝑦

Allowed substitution hints:   𝑆(𝑥, 𝑦, 𝑖, 𝑗, 𝑎)   𝑉(𝑥, 𝑦, 𝑖, 𝑗, 𝑎)   𝑊(𝑥, 𝑦, 𝑖, 𝑗, 𝑎)

Proof of Theorem satfv0

Dummy variables 𝑓 𝑚 𝑛 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano1 7924	. . . 4 ⊢ ∅ ∈ ω
2		elelsuc 6456	. . . 4 ⊢ (∅ ∈ ω → ∅ ∈ suc ω)
3	1, 2	mp1i 14	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ∅ ∈ suc ω)
4		satfv0.s	. . . 4 ⊢ 𝑆 = (𝑀 Sat 𝐸)
5	4	satfvsucom 36289	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ suc ω) → (𝑆‘∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅))
6	3, 5	mpd3an3 1492	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅))
7		goelel3xp 36280	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) ∈ (ω × (ω × ω)))
8		eleq1 2852	. . . . . . . . . 10 ⊢ (𝑥 = (𝑖∈𝑔𝑗) → (𝑥 ∈ (ω × (ω × ω)) ↔ (𝑖∈𝑔𝑗) ∈ (ω × (ω × ω))))
9	7, 8	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑥 = (𝑖∈𝑔𝑗) → 𝑥 ∈ (ω × (ω × ω))))
10	9	adantrd 497	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑥 ∈ (ω × (ω × ω))))
11	10	pm4.71d 571	. . . . . . 7 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω)))))
12	11	2rexbiia 3227	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω))))
13		r19.41vv 3236	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω))))
14		ancom 466	. . . . . 6 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω))) ↔ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
15	12, 13, 14	3bitri 300	. . . . 5 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
16	15	opabbii 5175	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))}
17		omex 9671	. . . . 5 ⊢ ω ∈ V
18	17, 17	xpex 7791	. . . . 5 ⊢ (ω × ω) ∈ V
19		xpexg 7788	. . . . . 6 ⊢ ((ω ∈ V ∧ (ω × ω) ∈ V) → (ω × (ω × ω)) ∈ V)
20		oveq1 7450	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑚 → (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑗))
21	20	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑚 → (𝑥 = (𝑖∈𝑔𝑗) ↔ 𝑥 = (𝑚∈𝑔𝑗)))
22		fveq2 6908	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑚 → (𝑎‘𝑖) = (𝑎‘𝑚))
23	22	breq1d 5116	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑚 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑎‘𝑚)𝐸(𝑎‘𝑗)))
24	23	rabbidv 3423	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑚 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)})
25	24	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑚 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)}))
26	21, 25	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑚∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)})))
27		oveq2 7451	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑛 → (𝑚∈𝑔𝑗) = (𝑚∈𝑔𝑛))
28	27	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑛 → (𝑥 = (𝑚∈𝑔𝑗) ↔ 𝑥 = (𝑚∈𝑔𝑛)))
29		fveq2 6908	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑛 → (𝑎‘𝑗) = (𝑎‘𝑛))
30	29	breq2d 5118	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑛 → ((𝑎‘𝑚)𝐸(𝑎‘𝑗) ↔ (𝑎‘𝑚)𝐸(𝑎‘𝑛)))
31	30	rabbidv 3423	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑛 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)})
32	31	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑛 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}))
33	28, 32	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑛 → ((𝑥 = (𝑚∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)})))
34	26, 33	cbvrex2vw 3249	. . . . . . . . . . 11 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}))
35		eqeq1 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑖∈𝑔𝑗) → (𝑥 = (𝑚∈𝑔𝑛) ↔ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)))
36	35	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑥 = (𝑚∈𝑔𝑛) ↔ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)))
37		goeleq12bg 36281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) ↔ (𝑖 = 𝑚 ∧ 𝑗 = 𝑛)))
38	22	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑚 → (𝑎‘𝑚) = (𝑎‘𝑖))
39	29	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 𝑛 → (𝑎‘𝑛) = (𝑎‘𝑗))
40	38, 39	breqan12d 5122	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 = 𝑚 ∧ 𝑗 = 𝑛) → ((𝑎‘𝑚)𝐸(𝑎‘𝑛) ↔ (𝑎‘𝑖)𝐸(𝑎‘𝑗)))
41	40	rabbidv 3423	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 = 𝑚 ∧ 𝑗 = 𝑛) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
42	37, 41	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
43	42	imp 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
44		eqeq12 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (𝑦 = 𝑧 ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
45	43, 44	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)) → ((𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧))
46	45	exp4b 436	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧))))
47	46	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧))))
48	36, 47	sylbid 243	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑥 = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧))))
49	48	impd 416	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧)))
50	49	com23 87	. . . . . . . . . . . . . . 15 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧)))
51	50	expimpd 459	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧)))
52	51	rexlimdvva 3223	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧)))
53	52	com23 87	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧)))
54	53	rexlimivv 3208	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧))
55	34, 54	sylbi 220	. . . . . . . . . 10 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧))
56	55	imp 412	. . . . . . . . 9 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧)
57	56	gen2 1829	. . . . . . . 8 ⊢ ∀𝑦∀𝑧((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧)
58		eqeq1 2767	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
59	58	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
60	59	2rexbidv 3231	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
61	60	mo4 2594	. . . . . . . 8 ⊢ (∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∀𝑦∀𝑧((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧))
62	57, 61	mpbir 234	. . . . . . 7 ⊢ ∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
63		moabex 5430	. . . . . . 7 ⊢ (∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → {𝑦 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V)
64	62, 63	mp1i 14	. . . . . 6 ⊢ (((ω ∈ V ∧ (ω × ω) ∈ V) ∧ 𝑥 ∈ (ω × (ω × ω))) → {𝑦 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V)
65	19, 64	opabex3d 8001	. . . . 5 ⊢ ((ω ∈ V ∧ (ω × ω) ∈ V) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))} ∈ V)
66	17, 18, 65	mp2an 705	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))} ∈ V
67	16, 66	eqeltri 2860	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V
68	67	rdg0 8457	. 2 ⊢ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}
69	6, 68	eqtrdi 2814	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570   ∈ wcel 2147  ∃*wmo 2565  {cab 2741  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  {csn 4588  ⟨cop 4838   class class class wbr 5106  {copab 5170   ↦ cmpt 5189   × cxp 5653   ↾ cres 5657  suc csuc 6382  ‘cfv 6558  (class class class)co 7443  ωcom 7901  1^st c1st 8023  2^nd c2nd 8024  reccrdg 8445   ↑_m cmap 8875  ∈_𝑔cgoe 36265  ⊼_𝑔cgna 36266  ∀_𝑔cgol 36267   Sat csat 36268

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-inf2 9669

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-goel 36272  df-sat 36275

This theorem is used by:  satfv1  36295  satfrel  36299  satfdm  36301  satfrnmapom  36302  satfv0fun  36303  satfv0fvfmla0  36345