satfrnmapom

Description: The range of the satisfaction predicate as function over wff codes in any model M and any binary relation E on M for a natural number N is a subset of the power set of all mappings from the natural numbers into the model M . (Contributed by AV, 13-Oct-2023)

		Ref	Expression
	Assertion	satfrnmapom	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ 𝒫 ( 𝑀 ↑_m ω ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑎 = ∅ → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
2	1	rneqd	⊢ ( 𝑎 = ∅ → ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ran ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
3	2	eleq2d	⊢ ( 𝑎 = ∅ → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) )
4	3	imbi1d	⊢ ( 𝑎 = ∅ → ( ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) )
5	4	imbi2d	⊢ ( 𝑎 = ∅ → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) )
6		fveq2	⊢ ( 𝑎 = 𝑏 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) )
7	6	rneqd	⊢ ( 𝑎 = 𝑏 → ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) )
8	7	eleq2d	⊢ ( 𝑎 = 𝑏 → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) )
9	8	imbi1d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) )
10	9	imbi2d	⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) )
11		fveq2	⊢ ( 𝑎 = suc 𝑏 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) )
12	11	rneqd	⊢ ( 𝑎 = suc 𝑏 → ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) )
13	12	eleq2d	⊢ ( 𝑎 = suc 𝑏 → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) )
14	13	imbi1d	⊢ ( 𝑎 = suc 𝑏 → ( ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) )
15	14	imbi2d	⊢ ( 𝑎 = suc 𝑏 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) )
16		fveq2	⊢ ( 𝑎 = 𝑁 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
17	16	rneqd	⊢ ( 𝑎 = 𝑁 → ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
18	17	eleq2d	⊢ ( 𝑎 = 𝑁 → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
19	18	imbi1d	⊢ ( 𝑎 = 𝑁 → ( ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) )
20	19	imbi2d	⊢ ( 𝑎 = 𝑁 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) )
21		eqid	⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
22	21	satfv0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } )
23	22	rneqd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ran ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } )
24	23	eleq2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ 𝑛 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } ) )
25		rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } = { 𝑦 ∣ ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) }
26	25	eleq2i	⊢ ( 𝑛 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } ↔ 𝑛 ∈ { 𝑦 ∣ ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } )
27		vex	⊢ 𝑛 ∈ V
28		eqeq1	⊢ ( 𝑦 = 𝑛 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ↔ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) )
29	28	anbi2d	⊢ ( 𝑦 = 𝑛 → ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) )
30	29	2rexbidv	⊢ ( 𝑦 = 𝑛 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) )
31	30	exbidv	⊢ ( 𝑦 = 𝑛 → ( ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) )
32	27 31	elab	⊢ ( 𝑛 ∈ { 𝑦 ∣ ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } ↔ ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) )
33		ovex	⊢ ( 𝑀 ↑_m ω ) ∈ V
34		ssrab2	⊢ { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ⊆ ( 𝑀 ↑_m ω )
35	33 34	elpwi2	⊢ { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ∈ 𝒫 ( 𝑀 ↑_m ω )
36		eleq1	⊢ ( 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } → ( 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ↔ { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
37	35 36	mpbiri	⊢ ( 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
38	37	adantl	⊢ ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
39	38	a1i	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
40	39	rexlimivv	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
41	40	exlimiv	⊢ ( ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑛 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
42	32 41	sylbi	⊢ ( 𝑛 ∈ { 𝑦 ∣ ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
43	42	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ { 𝑦 ∣ ∃ 𝑥 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
44	26 43	biimtrid	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
45	24 44	sylbid	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
46	21	satfvsuc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑏 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
47	46	3expa	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
48	47	rneqd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) → ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) = ran ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
49		rnun	⊢ ran ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) = ( ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } )
50	48 49	eqtrdi	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) → ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) = ( ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
51	50	eleq2d	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ↔ 𝑛 ∈ ( ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) )
52		elun	⊢ ( 𝑛 ∈ ( ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ 𝑛 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
53		rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } = { 𝑦 ∣ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) }
54	53	eleq2i	⊢ ( 𝑛 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ↔ 𝑛 ∈ { 𝑦 ∣ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } )
55		eqeq1	⊢ ( 𝑦 = 𝑛 → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ↔ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
56	55	anbi2d	⊢ ( 𝑦 = 𝑛 → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) )
57	56	rexbidv	⊢ ( 𝑦 = 𝑛 → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) )
58		eqeq1	⊢ ( 𝑦 = 𝑛 → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ↔ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) )
59	58	anbi2d	⊢ ( 𝑦 = 𝑛 → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
60	59	rexbidv	⊢ ( 𝑦 = 𝑛 → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
61	57 60	orbi12d	⊢ ( 𝑦 = 𝑛 → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
62	61	rexbidv	⊢ ( 𝑦 = 𝑛 → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
63	62	exbidv	⊢ ( 𝑦 = 𝑛 → ( ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
64	27 63	elab	⊢ ( 𝑛 ∈ { 𝑦 ∣ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ↔ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
65	54 64	bitri	⊢ ( 𝑛 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ↔ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
66	65	orbi2i	⊢ ( ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ 𝑛 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
67	52 66	bitri	⊢ ( 𝑛 ∈ ( ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
68	51 67	bitrdi	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) )
69	68	expcom	⊢ ( 𝑏 ∈ ω → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) ) )
70	69	adantr	⊢ ( ( 𝑏 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) ) )
71	70	imp	⊢ ( ( ( 𝑏 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ↔ ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) ) )
72		simpr	⊢ ( ( 𝑏 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) )
73	72	imp	⊢ ( ( ( 𝑏 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
74		difss	⊢ ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ⊆ ( 𝑀 ↑_m ω )
75	33 74	elpwi2	⊢ ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ∈ 𝒫 ( 𝑀 ↑_m ω )
76		eleq1	⊢ ( 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) → ( 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ↔ ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
77	75 76	mpbiri	⊢ ( 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
78	77	adantl	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
79	78	adantl	⊢ ( ( 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
80	79	rexlimiva	⊢ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
81		ssrab2	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ⊆ ( 𝑀 ↑_m ω )
82	33 81	elpwi2	⊢ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ∈ 𝒫 ( 𝑀 ↑_m ω )
83		eleq1	⊢ ( 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → ( 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ↔ { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
84	82 83	mpbiri	⊢ ( 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
85	84	adantl	⊢ ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
86	85	a1i	⊢ ( 𝑖 ∈ ω → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
87	86	rexlimiv	⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
88	80 87	jaoi	⊢ ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
89	88	a1i	⊢ ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
90	89	rexlimiv	⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
91	90	exlimiv	⊢ ( ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) )
92	91	a1i	⊢ ( ( ( 𝑏 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
93	73 92	jaod	⊢ ( ( ( 𝑏 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∨ ∃ 𝑥 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑛 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑛 = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
94	71 93	sylbid	⊢ ( ( ( 𝑏 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
95	94	exp31	⊢ ( 𝑏 ∈ ω → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) ) )
96	5 10 15 20 45 95	finds	⊢ ( 𝑁 ∈ ω → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) )
97	96	com12	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑁 ∈ ω → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) ) )
98	97	3impia	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( 𝑛 ∈ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → 𝑛 ∈ 𝒫 ( 𝑀 ↑_m ω ) ) )
99	98	ssrdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ 𝒫 ( 𝑀 ↑_m ω ) )

Metamath Proof Explorer

Theorem satfrnmapom

Proof