Theorem satfrnmapom 35875

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

Assertion

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

Proof of Theorem satfrnmapom

Dummy variables 𝑎 𝑏 𝑓 𝑖 𝑗 𝑢 𝑣 𝑥 𝑦 𝑧 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6885	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘∅))
2	1	rneqd 5930	. . . . . . . 8 ⊢ (𝑎 = ∅ → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘∅))
3	2	eleq2d 2851	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) ↔ 𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅)))
4	3	imbi1d 344	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
5	4	imbi2d 343	. . . . 5 ⊢ (𝑎 = ∅ → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) ↔ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
6		fveq2 6885	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑏))
7	6	rneqd 5930	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑏))
8	7	eleq2d 2851	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) ↔ 𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏)))
9	8	imbi1d 344	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
10	9	imbi2d 343	. . . . 5 ⊢ (𝑎 = 𝑏 → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) ↔ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
11		fveq2 6885	. . . . . . . . 9 ⊢ (𝑎 = suc 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘suc 𝑏))
12	11	rneqd 5930	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘suc 𝑏))
13	12	eleq2d 2851	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) ↔ 𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏)))
14	13	imbi1d 344	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
15	14	imbi2d 343	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) ↔ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
16		fveq2 6885	. . . . . . . . 9 ⊢ (𝑎 = 𝑁 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑁))
17	16	rneqd 5930	. . . . . . . 8 ⊢ (𝑎 = 𝑁 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑁))
18	17	eleq2d 2851	. . . . . . 7 ⊢ (𝑎 = 𝑁 → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) ↔ 𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁)))
19	18	imbi1d 344	. . . . . 6 ⊢ (𝑎 = 𝑁 → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
20	19	imbi2d 343	. . . . 5 ⊢ (𝑎 = 𝑁 → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) ↔ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
21		eqid 2765	. . . . . . . . 9 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
22	21	satfv0 35863	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
23	22	rneqd 5930	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ran ((𝑀 Sat 𝐸)‘∅) = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
24	23	eleq2d 2851	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) ↔ 𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}))
25		rnopab 5946	. . . . . . . 8 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} = {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}
26	25	eleq2i 2857	. . . . . . 7 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
27		vex 3461	. . . . . . . . . 10 ⊢ 𝑛 ∈ V
28		eqeq1 2769	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ↔ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
29	28	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑛 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
30	29	2rexbidv 3232	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
31	30	exbidv 1954	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
32	27, 31	elab 3640	. . . . . . . . 9 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
33		ovex 7449	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ↑m ω) ∈ V
34		ssrab2 4035	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ⊆ (𝑀 ↑m ω)
35	33, 34	elpwi2 5308	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ∈ 𝒫 (𝑀 ↑m ω)
36		eleq1 2853	. . . . . . . . . . . . . 14 ⊢ (𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ∈ 𝒫 (𝑀 ↑m ω)))
37	35, 36	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
38	37	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
39	38	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
40	39	rexlimivv 3209	. . . . . . . . . 10 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
41	40	exlimiv 1963	. . . . . . . . 9 ⊢ (∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
42	32, 41	sylbi 220	. . . . . . . 8 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
43	42	a1i 11	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
44	26, 43	biimtrid 245	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
45	24, 44	sylbid 243	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
46	21	satfvsuc 35866	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑏 ∈ ω) → ((𝑀 Sat 𝐸)‘suc 𝑏) = (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
47	46	3expa 1136	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ((𝑀 Sat 𝐸)‘suc 𝑏) = (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
48	47	rneqd 5930	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = ran (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
49		rnun 6144	. . . . . . . . . . . . 13 ⊢ ran (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) = (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
50	48, 49	eqtrdi 2816	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
51	50	eleq2d 2851	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ 𝑛 ∈ (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})))
52		elun 4107	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ 𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
53		rnopab 5946	. . . . . . . . . . . . . . 15 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} = {𝑦 ∣ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}
54	53	eleq2i 2857	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
55		eqeq1 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑛 → (𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ↔ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))))
56	55	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ↔ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))))
57	56	rexbidv 3191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))))
58		eqeq1 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
59	58	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
60	59	rexbidv 3191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
61	57, 60	orbi12d 932	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑛 → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
62	61	rexbidv 3191	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑛 → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
63	62	exbidv 1954	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑛 → (∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
64	27, 63	elab 3640	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ↔ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
65	54, 64	bitri 278	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ↔ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
66	65	orbi2i 926	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ 𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
67	52, 66	bitri 278	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
68	51, 67	bitrdi 290	. . . . . . . . . 10 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))))
69	68	expcom 419	. . . . . . . . 9 ⊢ (𝑏 ∈ ω → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))))
70	69	adantr 486	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))))
71	70	imp 412	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))))
72		simpr 490	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
73	72	imp 412	. . . . . . . 8 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
74		difss 4090	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ⊆ (𝑀 ↑m ω)
75	33, 74	elpwi2 5308	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑m ω)
76		eleq1 2853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑m ω)))
77	75, 76	mpbiri 261	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
78	77	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
79	78	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
80	79	rexlimiva 3160	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
81		ssrab2 4035	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ⊆ (𝑀 ↑m ω)
82	33, 81	elpwi2 5308	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑m ω)
83		eleq1 2853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑m ω)))
84	82, 83	mpbiri 261	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
85	84	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
86	85	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
87	86	rexlimiv 3161	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
88	80, 87	jaoi 871	. . . . . . . . . . . 12 ⊢ ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
89	88	a1i 11	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
90	89	rexlimiv 3161	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
91	90	exlimiv 1963	. . . . . . . . 9 ⊢ (∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
92	91	a1i 11	. . . . . . . 8 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
93	73, 92	jaod 873	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
94	71, 93	sylbid 243	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
95	94	exp31 425	. . . . 5 ⊢ (𝑏 ∈ ω → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
96	5, 10, 15, 20, 45, 95	finds 7895	. . . 4 ⊢ (𝑁 ∈ ω → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
97	96	com12 33	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑁 ∈ ω → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
98	97	3impia 1135	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
99	98	ssrdv 3944	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → ran ((𝑀 Sat 𝐸)‘𝑁) ⊆ 𝒫 (𝑀 ↑m ω))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {cab 2743  ∀wral 3081  ∃wrex 3091  {crab 3418  Vcvv 3457   ∖ cdif 3903   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  𝒫 cpw 4564  {csn 4591  ⟨cop 4597   class class class wbr 5111  {copab 5175  ran crn 5664   ↾ cres 5665  suc csuc 6366  ‘cfv 6540  (class class class)co 7416  ωcom 7864  1^st c1st 7986  2^nd c2nd 7987   ↑_m cmap 8826  ∈_𝑔cgoe 35838  ⊼_𝑔cgna 35839  ∀_𝑔cgol 35840   Sat csat 35841

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-inf2 9613

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-goel 35845  df-sat 35848

This theorem is used by:  satff  35915