satfv0

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

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

Proof

Step	Hyp	Ref	Expression
1		satfv0.s	⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
2		peano1	⊢ ∅ ∈ ω
3		elelsuc	⊢ ( ∅ ∈ ω → ∅ ∈ suc ω )
4	2 3	mp1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ∅ ∈ suc ω )
5	1	satfvsucom	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ suc ω ) → ( 𝑆 ‘ ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ) ‘ ∅ ) )
6	4 5	mpd3an3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ) ‘ ∅ ) )
7		goelel3xp	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈_𝑔 𝑗 ) ∈ ( ω × ( ω × ω ) ) )
8		eleq1	⊢ ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) → ( 𝑥 ∈ ( ω × ( ω × ω ) ) ↔ ( 𝑖 ∈_𝑔 𝑗 ) ∈ ( ω × ( ω × ω ) ) ) )
9	7 8	syl5ibrcom	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) → 𝑥 ∈ ( ω × ( ω × ω ) ) ) )
10	9	adantrd	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → 𝑥 ∈ ( ω × ( ω × ω ) ) ) )
11	10	pm4.71d	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ 𝑥 ∈ ( ω × ( ω × ω ) ) ) ) )
12	11	2rexbiia	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ 𝑥 ∈ ( ω × ( ω × ω ) ) ) )
13		r19.41vv	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ 𝑥 ∈ ( ω × ( ω × ω ) ) ) ↔ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ 𝑥 ∈ ( ω × ( ω × ω ) ) ) )
14		ancom	⊢ ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ 𝑥 ∈ ( ω × ( ω × ω ) ) ) ↔ ( 𝑥 ∈ ( ω × ( ω × ω ) ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
15	12 13 14	3bitri	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑥 ∈ ( ω × ( ω × ω ) ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
16	15	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ω × ( ω × ω ) ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) }
17		omex	⊢ ω ∈ V
18	17 17	xpex	⊢ ( ω × ω ) ∈ V
19		xpexg	⊢ ( ( ω ∈ V ∧ ( ω × ω ) ∈ V ) → ( ω × ( ω × ω ) ) ∈ V )
20		oveq1	⊢ ( 𝑖 = 𝑚 → ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑗 ) )
21	20	eqeq2d	⊢ ( 𝑖 = 𝑚 → ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ↔ 𝑥 = ( 𝑚 ∈_𝑔 𝑗 ) ) )
22		fveq2	⊢ ( 𝑖 = 𝑚 → ( 𝑎 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑚 ) )
23	22	breq1d	⊢ ( 𝑖 = 𝑚 → ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ↔ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) )
24	23	rabbidv	⊢ ( 𝑖 = 𝑚 → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } )
25	24	eqeq2d	⊢ ( 𝑖 = 𝑚 → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
26	21 25	anbi12d	⊢ ( 𝑖 = 𝑚 → ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑚 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
27		oveq2	⊢ ( 𝑗 = 𝑛 → ( 𝑚 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) )
28	27	eqeq2d	⊢ ( 𝑗 = 𝑛 → ( 𝑥 = ( 𝑚 ∈_𝑔 𝑗 ) ↔ 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ) )
29		fveq2	⊢ ( 𝑗 = 𝑛 → ( 𝑎 ‘ 𝑗 ) = ( 𝑎 ‘ 𝑛 ) )
30	29	breq2d	⊢ ( 𝑗 = 𝑛 → ( ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ↔ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) ) )
31	30	rabbidv	⊢ ( 𝑗 = 𝑛 → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } )
32	31	eqeq2d	⊢ ( 𝑗 = 𝑛 → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ↔ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) )
33	28 32	anbi12d	⊢ ( 𝑗 = 𝑛 → ( ( 𝑥 = ( 𝑚 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) ) )
34	26 33	cbvrex2vw	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) )
35		eqeq1	⊢ ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) → ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ↔ ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) ) )
36	35	adantl	⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ∧ 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) → ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ↔ ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) ) )
37		goeleq12bg	⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) ↔ ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑛 ) ) )
38	22	eqcomd	⊢ ( 𝑖 = 𝑚 → ( 𝑎 ‘ 𝑚 ) = ( 𝑎 ‘ 𝑖 ) )
39	29	eqcomd	⊢ ( 𝑗 = 𝑛 → ( 𝑎 ‘ 𝑛 ) = ( 𝑎 ‘ 𝑗 ) )
40	38 39	breqan12d	⊢ ( ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑛 ) → ( ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) ↔ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) )
41	40	rabbidv	⊢ ( ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑛 ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } )
42	37 41	syl6bi	⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
43	42	imp	⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ∧ ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } )
44		eqeq12	⊢ ( ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( 𝑦 = 𝑧 ↔ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
45	43 44	syl5ibrcom	⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ∧ ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) ) → ( ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → 𝑦 = 𝑧 ) )
46	45	exp4b	⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } → ( 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) ) )
47	46	adantr	⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ∧ 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) → ( ( 𝑖 ∈_𝑔 𝑗 ) = ( 𝑚 ∈_𝑔 𝑛 ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } → ( 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) ) )
48	36 47	sylbid	⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ∧ 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) → ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } → ( 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) ) )
49	48	impd	⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ∧ 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) → ( ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) → ( 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) )
50	49	com23	⊢ ( ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ∧ 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) → ( 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } → ( ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) → 𝑦 = 𝑧 ) ) )
51	50	expimpd	⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) → 𝑦 = 𝑧 ) ) )
52	51	rexlimdvva	⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) → 𝑦 = 𝑧 ) ) )
53	52	com23	⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → 𝑦 = 𝑧 ) ) )
54	53	rexlimivv	⊢ ( ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑥 = ( 𝑚 ∈_𝑔 𝑛 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑚 ) 𝐸 ( 𝑎 ‘ 𝑛 ) } ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → 𝑦 = 𝑧 ) )
55	34 54	sylbi	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → 𝑦 = 𝑧 ) )
56	55	imp	⊢ ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) → 𝑦 = 𝑧 )
57	56	gen2	⊢ ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) → 𝑦 = 𝑧 )
58		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ↔ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) )
59	58	anbi2d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
60	59	2rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) )
61	60	mo4	⊢ ( ∃* 𝑦 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) → 𝑦 = 𝑧 ) )
62	57 61	mpbir	⊢ ∃* 𝑦 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } )
63		moabex	⊢ ( ∃* 𝑦 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) → { 𝑦 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ∈ V )
64	62 63	mp1i	⊢ ( ( ( ω ∈ V ∧ ( ω × ω ) ∈ V ) ∧ 𝑥 ∈ ( ω × ( ω × ω ) ) ) → { 𝑦 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ∈ V )
65	19 64	opabex3d	⊢ ( ( ω ∈ V ∧ ( ω × ω ) ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ω × ( ω × ω ) ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) } ∈ V )
66	17 18 65	mp2an	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ω × ( ω × ω ) ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) ) } ∈ V
67	16 66	eqeltri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ∈ V
68	67	rdg0	⊢ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) }
69	6 68	eqtrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } )

Metamath Proof Explorer

Theorem satfv0

Proof