Theorem satfrnmapom 36114

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 6883	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘∅))
2	1	rneqd 5920	. . . . . . . 8 ⊢ (𝑎 = ∅ → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘∅))
3	2	eleq2d 2847	. . . . . . 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 6883	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑏))
7	6	rneqd 5920	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑏))
8	7	eleq2d 2847	. . . . . . 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 6883	. . . . . . . . 9 ⊢ (𝑎 = suc 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘suc 𝑏))
12	11	rneqd 5920	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘suc 𝑏))
13	12	eleq2d 2847	. . . . . . 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 6883	. . . . . . . . 9 ⊢ (𝑎 = 𝑁 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑁))
17	16	rneqd 5920	. . . . . . . 8 ⊢ (𝑎 = 𝑁 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑁))
18	17	eleq2d 2847	. . . . . . 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 2761	. . . . . . . . 9 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
22	21	satfv0 36102	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
23	22	rneqd 5920	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ran ((𝑀 Sat 𝐸)‘∅) = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
24	23	eleq2d 2847	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) ↔ 𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}))
25		rnopab 5936	. . . . . . . 8 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} = {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}
26	25	eleq2i 2853	. . . . . . 7 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
27		vex 3455	. . . . . . . . . 10 ⊢ 𝑛 ∈ V
28		eqeq1 2765	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ↔ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
29	28	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑛 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
30	29	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
31	30	exbidv 1954	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
32	27, 31	elab 3633	. . . . . . . . 9 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
33		ovex 7451	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ↑m ω) ∈ V
34		ssrab2 4028	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ⊆ (𝑀 ↑m ω)
35	33, 34	elpwi2 5297	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ∈ 𝒫 (𝑀 ↑m ω)
36		eleq1 2849	. . . . . . . . . . . . . 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 3205	. . . . . . . . . 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 36105	. . . . . . . . . . . . . . 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 5920	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = ran (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
49		rnun 6136	. . . . . . . . . . . . 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 2812	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
51	50	eleq2d 2847	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ 𝑛 ∈ (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})))
52		elun 4100	. . . . . . . . . . . 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 5936	. . . . . . . . . . . . . . 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 2853	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
55		eqeq1 2765	. . . . . . . . . . . . . . . . . . . 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 3187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))))
58		eqeq1 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
59	58	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
60	59	rexbidv 3187	. . . . . . . . . . . . . . . . . 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 3187	. . . . . . . . . . . . . . . 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 3633	. . . . . . . . . . . . . 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 4083	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ⊆ (𝑀 ↑m ω)
75	33, 74	elpwi2 5297	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑m ω)
76		eleq1 2849	. . . . . . . . . . . . . . . . 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 3156	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
81		ssrab2 4028	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ⊆ (𝑀 ↑m ω)
82	33, 81	elpwi2 5297	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑m ω)
83		eleq1 2849	. . . . . . . . . . . . . . . . 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 3157	. . . . . . . . . . . . 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 3157	. . . . . . . . . 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 7906	. . . 4 ⊢ (𝑁 ∈ ω → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
97	96	com12 33	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑁 ∈ ω → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
98	97	3impia 1135	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
99	98	ssrdv 3937	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 2145  {cab 2739  ∀wral 3077  ∃wrex 3087  {crab 3413  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584  ⟨cop 4590   class class class wbr 5103  {copab 5167  ran crn 5652   ↾ cres 5653  suc csuc 6363  ‘cfv 6537  (class class class)co 7418  ωcom 7875  1^st c1st 7997  2^nd c2nd 7998   ↑_m cmap 8840  ∈_𝑔cgoe 36077  ⊼_𝑔cgna 36078  ∀_𝑔cgol 36079   Sat csat 36080

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-inf2 9635

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-goel 36084  df-sat 36087

This theorem is used by:  satff  36154