Theorem satfrnmapom 35583

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 6842	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘∅))
2	1	rneqd 5895	. . . . . . . 8 ⊢ (𝑎 = ∅ → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘∅))
3	2	eleq2d 2823	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) ↔ 𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅)))
4	3	imbi1d 341	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
5	4	imbi2d 340	. . . . 5 ⊢ (𝑎 = ∅ → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) ↔ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
6		fveq2 6842	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑏))
7	6	rneqd 5895	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑏))
8	7	eleq2d 2823	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) ↔ 𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏)))
9	8	imbi1d 341	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
10	9	imbi2d 340	. . . . 5 ⊢ (𝑎 = 𝑏 → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) ↔ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
11		fveq2 6842	. . . . . . . . 9 ⊢ (𝑎 = suc 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘suc 𝑏))
12	11	rneqd 5895	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘suc 𝑏))
13	12	eleq2d 2823	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) ↔ 𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏)))
14	13	imbi1d 341	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
15	14	imbi2d 340	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) ↔ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
16		fveq2 6842	. . . . . . . . 9 ⊢ (𝑎 = 𝑁 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑁))
17	16	rneqd 5895	. . . . . . . 8 ⊢ (𝑎 = 𝑁 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑁))
18	17	eleq2d 2823	. . . . . . 7 ⊢ (𝑎 = 𝑁 → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) ↔ 𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁)))
19	18	imbi1d 341	. . . . . 6 ⊢ (𝑎 = 𝑁 → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
20	19	imbi2d 340	. . . . 5 ⊢ (𝑎 = 𝑁 → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑎) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) ↔ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
21		eqid 2737	. . . . . . . . 9 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
22	21	satfv0 35571	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
23	22	rneqd 5895	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ran ((𝑀 Sat 𝐸)‘∅) = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
24	23	eleq2d 2823	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) ↔ 𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}))
25		rnopab 5911	. . . . . . . 8 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} = {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}
26	25	eleq2i 2829	. . . . . . 7 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
27		vex 3446	. . . . . . . . . 10 ⊢ 𝑛 ∈ V
28		eqeq1 2741	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ↔ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
29	28	anbi2d 631	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑛 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
30	29	2rexbidv 3203	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
31	30	exbidv 1923	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
32	27, 31	elab 3636	. . . . . . . . 9 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
33		ovex 7401	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ↑m ω) ∈ V
34		ssrab2 4034	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ⊆ (𝑀 ↑m ω)
35	33, 34	elpwi2 5282	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ∈ 𝒫 (𝑀 ↑m ω)
36		eleq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ∈ 𝒫 (𝑀 ↑m ω)))
37	35, 36	mpbiri 258	. . . . . . . . . . . . 13 ⊢ (𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
38	37	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
39	38	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
40	39	rexlimivv 3180	. . . . . . . . . 10 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
41	40	exlimiv 1932	. . . . . . . . 9 ⊢ (∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
42	32, 41	sylbi 217	. . . . . . . 8 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
43	42	a1i 11	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
44	26, 43	biimtrid 242	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
45	24, 44	sylbid 240	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
46	21	satfvsuc 35574	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑏 ∈ ω) → ((𝑀 Sat 𝐸)‘suc 𝑏) = (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
47	46	3expa 1119	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ((𝑀 Sat 𝐸)‘suc 𝑏) = (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
48	47	rneqd 5895	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = ran (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
49		rnun 6111	. . . . . . . . . . . . 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 2788	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
51	50	eleq2d 2823	. . . . . . . . . . 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 5911	. . . . . . . . . . . . . . 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 2829	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
55		eqeq1 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑛 → (𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ↔ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))))
56	55	anbi2d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ↔ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))))
57	56	rexbidv 3162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))))
58		eqeq1 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
59	58	anbi2d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
60	59	rexbidv 3162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
61	57, 60	orbi12d 919	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑛 → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
62	61	rexbidv 3162	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑛 → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
63	62	exbidv 1923	. . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . 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 913	. . . . . . . . . . . 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 275	. . . . . . . . . . 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 287	. . . . . . . . . 10 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))))
69	68	expcom 413	. . . . . . . . 9 ⊢ (𝑏 ∈ ω → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))))
70	69	adantr 480	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))))
71	70	imp 406	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))))
72		simpr 484	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
73	72	imp 406	. . . . . . . 8 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
74		difss 4090	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ⊆ (𝑀 ↑m ω)
75	33, 74	elpwi2 5282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑m ω)
76		eleq1 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑m ω)))
77	75, 76	mpbiri 258	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
78	77	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
79	78	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
80	79	rexlimiva 3131	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
81		ssrab2 4034	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ⊆ (𝑀 ↑m ω)
82	33, 81	elpwi2 5282	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑m ω)
83		eleq1 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑m ω)))
84	82, 83	mpbiri 258	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
85	84	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
86	85	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
87	86	rexlimiv 3132	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
88	80, 87	jaoi 858	. . . . . . . . . . . 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 3132	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
91	90	exlimiv 1932	. . . . . . . . 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 860	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
94	71, 93	sylbid 240	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
95	94	exp31 419	. . . . 5 ⊢ (𝑏 ∈ ω → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
96	5, 10, 15, 20, 45, 95	finds 7848	. . . 4 ⊢ (𝑁 ∈ ω → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
97	96	com12 32	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑁 ∈ ω → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
98	97	3impia 1118	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
99	98	ssrdv 3941	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → ran ((𝑀 Sat 𝐸)‘𝑁) ⊆ 𝒫 (𝑀 ↑m ω))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556  {csn 4582  ⟨cop 4588   class class class wbr 5100  {copab 5162  ran crn 5633   ↾ cres 5634  suc csuc 6327  ‘cfv 6500  (class class class)co 7368  ωcom 7818  1^st c1st 7941  2^nd c2nd 7942   ↑_m cmap 8775  ∈_𝑔cgoe 35546  ⊼_𝑔cgna 35547  ∀_𝑔cgol 35548   Sat csat 35549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-inf2 9562

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-goel 35553  df-sat 35556

This theorem is referenced by:  satff  35623