Theorem satfv0 35001

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 7900	. . . 4 ⊢ ∅ ∈ ω
2		elelsuc 6447	. . . 4 ⊢ (∅ ∈ ω → ∅ ∈ suc ω)
3	1, 2	mp1i 13	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ∅ ∈ suc ω)
4		satfv0.s	. . . 4 ⊢ 𝑆 = (𝑀 Sat 𝐸)
5	4	satfvsucom 35000	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ suc ω) → (𝑆‘∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅))
6	3, 5	mpd3an3 1458	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅))
7		goelel3xp 34991	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) ∈ (ω × (ω × ω)))
8		eleq1 2817	. . . . . . . . . 10 ⊢ (𝑥 = (𝑖∈𝑔𝑗) → (𝑥 ∈ (ω × (ω × ω)) ↔ (𝑖∈𝑔𝑗) ∈ (ω × (ω × ω))))
9	7, 8	syl5ibrcom 246	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑥 = (𝑖∈𝑔𝑗) → 𝑥 ∈ (ω × (ω × ω))))
10	9	adantrd 490	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑥 ∈ (ω × (ω × ω))))
11	10	pm4.71d 560	. . . . . . 7 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω)))))
12	11	2rexbiia 3213	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω))))
13		r19.41vv 3222	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω))))
14		ancom 459	. . . . . 6 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ 𝑥 ∈ (ω × (ω × ω))) ↔ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
15	12, 13, 14	3bitri 296	. . . . 5 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
16	15	opabbii 5219	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))}
17		omex 9674	. . . . 5 ⊢ ω ∈ V
18	17, 17	xpex 7761	. . . . 5 ⊢ (ω × ω) ∈ V
19		xpexg 7758	. . . . . 6 ⊢ ((ω ∈ V ∧ (ω × ω) ∈ V) → (ω × (ω × ω)) ∈ V)
20		oveq1 7433	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑚 → (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑗))
21	20	eqeq2d 2739	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑚 → (𝑥 = (𝑖∈𝑔𝑗) ↔ 𝑥 = (𝑚∈𝑔𝑗)))
22		fveq2 6902	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑚 → (𝑎‘𝑖) = (𝑎‘𝑚))
23	22	breq1d 5162	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑚 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑎‘𝑚)𝐸(𝑎‘𝑗)))
24	23	rabbidv 3438	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑚 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)})
25	24	eqeq2d 2739	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑚 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)}))
26	21, 25	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑚∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)})))
27		oveq2 7434	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑛 → (𝑚∈𝑔𝑗) = (𝑚∈𝑔𝑛))
28	27	eqeq2d 2739	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑛 → (𝑥 = (𝑚∈𝑔𝑗) ↔ 𝑥 = (𝑚∈𝑔𝑛)))
29		fveq2 6902	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑛 → (𝑎‘𝑗) = (𝑎‘𝑛))
30	29	breq2d 5164	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑛 → ((𝑎‘𝑚)𝐸(𝑎‘𝑗) ↔ (𝑎‘𝑚)𝐸(𝑎‘𝑛)))
31	30	rabbidv 3438	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑛 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)})
32	31	eqeq2d 2739	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑛 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}))
33	28, 32	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑛 → ((𝑥 = (𝑚∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)})))
34	26, 33	cbvrex2vw 3237	. . . . . . . . . . 11 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}))
35		eqeq1 2732	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑖∈𝑔𝑗) → (𝑥 = (𝑚∈𝑔𝑛) ↔ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)))
36	35	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑥 = (𝑚∈𝑔𝑛) ↔ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)))
37		goeleq12bg 34992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) ↔ (𝑖 = 𝑚 ∧ 𝑗 = 𝑛)))
38	22	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑚 → (𝑎‘𝑚) = (𝑎‘𝑖))
39	29	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 𝑛 → (𝑎‘𝑛) = (𝑎‘𝑗))
40	38, 39	breqan12d 5168	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 = 𝑚 ∧ 𝑗 = 𝑛) → ((𝑎‘𝑚)𝐸(𝑎‘𝑛) ↔ (𝑎‘𝑖)𝐸(𝑎‘𝑗)))
41	40	rabbidv 3438	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 = 𝑚 ∧ 𝑗 = 𝑛) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
42	37, 41	biimtrdi 252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
43	42	imp 405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)) → {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
44		eqeq12 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (𝑦 = 𝑧 ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
45	43, 44	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ (𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛)) → ((𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧))
46	45	exp4b 429	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧))))
47	46	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → ((𝑖∈𝑔𝑗) = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧))))
48	36, 47	sylbid 239	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑥 = (𝑚∈𝑔𝑛) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)} → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧))))
49	48	impd 409	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → 𝑦 = 𝑧)))
50	49	com23 86	. . . . . . . . . . . . . . 15 ⊢ ((((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) ∧ 𝑥 = (𝑖∈𝑔𝑗)) → (𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧)))
51	50	expimpd 452	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ω ∧ 𝑛 ∈ ω) ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧)))
52	51	rexlimdvva 3209	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → 𝑦 = 𝑧)))
53	52	com23 86	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧)))
54	53	rexlimivv 3197	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑥 = (𝑚∈𝑔𝑛) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑚)𝐸(𝑎‘𝑛)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧))
55	34, 54	sylbi 216	. . . . . . . . . 10 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → 𝑦 = 𝑧))
56	55	imp 405	. . . . . . . . 9 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧)
57	56	gen2 1790	. . . . . . . 8 ⊢ ∀𝑦∀𝑧((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧)
58		eqeq1 2732	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
59	58	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
60	59	2rexbidv 3217	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
61	60	mo4 2555	. . . . . . . 8 ⊢ (∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ∀𝑦∀𝑧((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑧 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → 𝑦 = 𝑧))
62	57, 61	mpbir 230	. . . . . . 7 ⊢ ∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
63		moabex 5465	. . . . . . 7 ⊢ (∃*𝑦∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → {𝑦 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V)
64	62, 63	mp1i 13	. . . . . 6 ⊢ (((ω ∈ V ∧ (ω × ω) ∈ V) ∧ 𝑥 ∈ (ω × (ω × ω))) → {𝑦 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V)
65	19, 64	opabex3d 7975	. . . . 5 ⊢ ((ω ∈ V ∧ (ω × ω) ∈ V) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))} ∈ V)
66	17, 18, 65	mp2an 690	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (ω × (ω × ω)) ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))} ∈ V
67	16, 66	eqeltri 2825	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} ∈ V
68	67	rdg0 8448	. 2 ⊢ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}
69	6, 68	eqtrdi 2784	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845  ∀wal 1531   = wceq 1533   ∈ wcel 2098  ∃*wmo 2527  {cab 2705  ∀wral 3058  ∃wrex 3067  {crab 3430  Vcvv 3473   ∖ cdif 3946   ∪ cun 3947   ∩ cin 3948  ∅c0 4326  {csn 4632  ⟨cop 4638   class class class wbr 5152  {copab 5214   ↦ cmpt 5235   × cxp 5680   ↾ cres 5684  suc csuc 6376  ‘cfv 6553  (class class class)co 7426  ωcom 7876  1^st c1st 7997  2^nd c2nd 7998  reccrdg 8436   ↑_m cmap 8851  ∈_𝑔cgoe 34976  ⊼_𝑔cgna 34977  ∀_𝑔cgol 34978   Sat csat 34979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-goel 34983  df-sat 34986

This theorem is referenced by:  satfv1  35006  satfrel  35010  satfdm  35012  satfrnmapom  35013  satfv0fun  35014  satfv0fvfmla0  35056