Theorem satfrnmapom 32617

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 6670	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘∅))
2	1	rneqd 5808	. . . . . . . 8 ⊢ (𝑎 = ∅ → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘∅))
3	2	eleq2d 2898	. . . . . . 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 6670	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑏))
7	6	rneqd 5808	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑏))
8	7	eleq2d 2898	. . . . . . 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 6670	. . . . . . . . 9 ⊢ (𝑎 = suc 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘suc 𝑏))
12	11	rneqd 5808	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘suc 𝑏))
13	12	eleq2d 2898	. . . . . . 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 6670	. . . . . . . . 9 ⊢ (𝑎 = 𝑁 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑁))
17	16	rneqd 5808	. . . . . . . 8 ⊢ (𝑎 = 𝑁 → ran ((𝑀 Sat 𝐸)‘𝑎) = ran ((𝑀 Sat 𝐸)‘𝑁))
18	17	eleq2d 2898	. . . . . . 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 2821	. . . . . . . . 9 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
22	21	satfv0 32605	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
23	22	rneqd 5808	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ran ((𝑀 Sat 𝐸)‘∅) = ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
24	23	eleq2d 2898	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) ↔ 𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}))
25		rnopab 5826	. . . . . . . 8 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} = {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})}
26	25	eleq2i 2904	. . . . . . 7 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})})
27		vex 3497	. . . . . . . . . 10 ⊢ 𝑛 ∈ V
28		eqeq1 2825	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ↔ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
29	28	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑛 → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
30	29	2rexbidv 3300	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
31	30	exbidv 1922	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})))
32	27, 31	elab 3667	. . . . . . . . 9 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} ↔ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}))
33		ovex 7189	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ↑m ω) ∈ V
34		ssrab2 4056	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ⊆ (𝑀 ↑m ω)
35	33, 34	elpwi2 5249	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ∈ 𝒫 (𝑀 ↑m ω)
36		eleq1 2900	. . . . . . . . . . . . . 14 ⊢ (𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} ∈ 𝒫 (𝑀 ↑m ω)))
37	35, 36	mpbiri 260	. . . . . . . . . . . . 13 ⊢ (𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
38	37	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
39	38	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
40	39	rexlimivv 3292	. . . . . . . . . 10 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
41	40	exlimiv 1931	. . . . . . . . 9 ⊢ (∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑛 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
42	32, 41	sylbi 219	. . . . . . . 8 ⊢ (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
43	42	a1i 11	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
44	26, 43	syl5bi 244	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ (𝑓‘𝑖)𝐸(𝑓‘𝑗)})} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
45	24, 44	sylbid 242	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘∅) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
46	21	satfvsuc 32608	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑏 ∈ ω) → ((𝑀 Sat 𝐸)‘suc 𝑏) = (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
47	46	3expa 1114	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ((𝑀 Sat 𝐸)‘suc 𝑏) = (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
48	47	rneqd 5808	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = ran (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
49		rnun 6004	. . . . . . . . . . . . 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	syl6eq 2872	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → ran ((𝑀 Sat 𝐸)‘suc 𝑏) = (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
51	50	eleq2d 2898	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ 𝑛 ∈ (ran ((𝑀 Sat 𝐸)‘𝑏) ∪ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})))
52		elun 4125	. . . . . . . . . . . 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 5826	. . . . . . . . . . . . . . 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 2904	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ran {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ↔ 𝑛 ∈ {𝑦 ∣ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
55		eqeq1 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑛 → (𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ↔ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))))
56	55	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ↔ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))))
57	56	rexbidv 3297	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))))
58		eqeq1 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑛 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
59	58	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
60	59	rexbidv 3297	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))
61	57, 60	orbi12d 915	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑛 → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
62	61	rexbidv 3297	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑛 → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))
63	62	exbidv 1922	. . . . . . . . . . . . . . 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 3667	. . . . . . . . . . . . . 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 277	. . . . . . . . . . . . 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 909	. . . . . . . . . . . 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 277	. . . . . . . . . . 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	syl6bb 289	. . . . . . . . . 10 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑏 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))))
69	68	expcom 416	. . . . . . . . 9 ⊢ (𝑏 ∈ ω → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))))
70	69	adantr 483	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))))
71	70	imp 409	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))))
72		simpr 487	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
73	72	imp 409	. . . . . . . 8 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
74		difss 4108	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ⊆ (𝑀 ↑m ω)
75	33, 74	elpwi2 5249	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑m ω)
76		eleq1 2900	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑m ω)))
77	75, 76	mpbiri 260	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
78	77	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
79	78	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
80	79	rexlimiva 3281	. . . . . . . . . . . . 13 ⊢ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
81		ssrab2 4056	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ⊆ (𝑀 ↑m ω)
82	33, 81	elpwi2 5249	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑m ω)
83		eleq1 2900	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → (𝑛 ∈ 𝒫 (𝑀 ↑m ω) ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑m ω)))
84	82, 83	mpbiri 260	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
85	84	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
86	85	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
87	86	rexlimiv 3280	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
88	80, 87	jaoi 853	. . . . . . . . . . . 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 3280	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))
91	90	exlimiv 1931	. . . . . . . . 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 855	. . . . . . 7 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) ∨ ∃𝑥∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑛 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑛 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
94	71, 93	sylbid 242	. . . . . 6 ⊢ (((𝑏 ∈ ω ∧ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))) ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
95	94	exp31 422	. . . . 5 ⊢ (𝑏 ∈ ω → (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘suc 𝑏) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))))
96	5, 10, 15, 20, 45, 95	finds 7608	. . . 4 ⊢ (𝑁 ∈ ω → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
97	96	com12 32	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑁 ∈ ω → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω))))
98	97	3impia 1113	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → (𝑛 ∈ ran ((𝑀 Sat 𝐸)‘𝑁) → 𝑛 ∈ 𝒫 (𝑀 ↑m ω)))
99	98	ssrdv 3973	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → ran ((𝑀 Sat 𝐸)‘𝑁) ⊆ 𝒫 (𝑀 ↑m ω))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2799  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3494   ∖ cdif 3933   ∪ cun 3934   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539  {csn 4567  ⟨cop 4573   class class class wbr 5066  {copab 5128  ran crn 5556   ↾ cres 5557  suc csuc 6193  ‘cfv 6355  (class class class)co 7156  ωcom 7580  1^st c1st 7687  2^nd c2nd 7688   ↑_m cmap 8406  ∈_𝑔cgoe 32580  ⊼_𝑔cgna 32581  ∀_𝑔cgol 32582   Sat csat 32583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-inf2 9104

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-goel 32587  df-sat 32590

This theorem is referenced by:  satff  32657