Theorem satfrnmapom 36336

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 6914	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘∅))
2	1	rneqd 5930	. . . . . . . 8 ⊢ (𝑎 = ∅ → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘∅))
3	2	eleq2d 2850	. . . . . . 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 6914	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑏))
7	6	rneqd 5930	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑏))
8	7	eleq2d 2850	. . . . . . 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 6914	. . . . . . . . 9 ⊢ (𝑎 = suc 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘suc 𝑏))
12	11	rneqd 5930	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘suc 𝑏))
13	12	eleq2d 2850	. . . . . . 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 6914	. . . . . . . . 9 ⊢ (𝑎 = 𝑁 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑁))
17	16	rneqd 5930	. . . . . . . 8 ⊢ (𝑎 = 𝑁 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑁))
18	17	eleq2d 2850	. . . . . . 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 2763	. . . . . . . . 9 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
22	21	satfv0 36324	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
23	22	rneqd 5930	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ran ((𝑀 Sat 𝐸)‘∅) = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
24	23	eleq2d 2850	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) ↔ 𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}))
25		rnopab 5946	. . . . . . . 8 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} = {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}
26	25	eleq2i 2856	. . . . . . 7 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
27		vex 3458	. . . . . . . . . 10 ⊢ 𝑛 ∈ V
28		eqeq1 2767	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ↔ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
29	28	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑛 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
30	29	2rexbidv 3231	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
31	30	exbidv 1956	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
32	27, 31	elab 3636	. . . . . . . . 9 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
33		ovex 7482	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ↑m ω) ∈ V
34		ssrab2 4008	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ⊆ (𝑀 ↑m ω)
35	33, 34	elpwi2 5302	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ∈ 𝒫 (𝑀 ↑m ω)
36		eleq1 2852	. . . . . . . . . . . . . 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 3208	. . . . . . . . . 10 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
41	40	exlimiv 1965	. . . . . . . . 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 36327	. . . . . . . . . . . . . . 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 6152	. . . . . . . . . . . . 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 2814	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
51	50	eleq2d 2850	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ 𝑛 ∈ (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})))
52		elun 4155	. . . . . . . . . . . 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 2856	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
55		eqeq1 2767	. . . . . . . . . . . . . . . . . . . 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 3190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))))
58		eqeq1 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
59	58	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
60	59	rexbidv 3190	. . . . . . . . . . . . . . . . . 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 3190	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑛 → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
63	62	exbidv 1956	. . . . . . . . . . . . . . 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 3636	. . . . . . . . . . . . . 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 4075	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ⊆ (𝑀 ↑m ω)
75	33, 74	elpwi2 5302	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑m ω)
76		eleq1 2852	. . . . . . . . . . . . . . . . 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 3159	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
81		ssrab2 4008	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ⊆ (𝑀 ↑m ω)
82	33, 81	elpwi2 5302	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑m ω)
83		eleq1 2852	. . . . . . . . . . . . . . . . 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 3160	. . . . . . . . . . . . 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 3160	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
91	90	exlimiv 1965	. . . . . . . . 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 7940	. . . 4 ⊢ (𝑁 ∈ ω → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
97	96	com12 33	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑁 ∈ ω → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
98	97	3impia 1135	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
99	98	ssrdv 3919	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 2147  {cab 2741  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  𝒫 cpw 4560  {csn 4588  ⟨cop 4838   class class class wbr 5106  {copab 5171  ran crn 5657   ↾ cres 5658  suc csuc 6388  ‘cfv 6564  (class class class)co 7449  ωcom 7909  1^st c1st 8031  2^nd c2nd 8032   ↑_m cmap 8883  ∈_𝑔cgoe 36299  ⊼_𝑔cgna 36300  ∀_𝑔cgol 36301   Sat csat 36302

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 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-inf2 9677

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 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6328  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-ov 7452  df-oprab 7453  df-mpo 7454  df-om 7910  df-2nd 8034  df-frecs 8335  df-wrecs 8366  df-recs 8415  df-rdg 8454  df-goel 36306  df-sat 36309

This theorem is used by:  satff  36376