satffunlem2 - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > satffunlem2		Structured version Visualization version GIF version

Theorem satffunlem2 36260

Description: Lemma 2 for satffun 36261: induction step. (Contributed by AV, 28-Oct-2023.)

**Assertion**
Ref	Expression
satffunlem2	⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁)))

Proof of Theorem satffunlem2 Dummy variables 𝑓 𝑖 𝑗 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 490	. . . 4 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁))
2		simpr 490	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊))
3		peano2 7902	. . . . . . . . 9 ⊢ (𝑁 ∈ ω → suc 𝑁 ∈ ω)
4	3	ancri 559	. . . . . . . 8 ⊢ (𝑁 ∈ ω → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
5	4	adantr 486	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))
6		sssucid 6445	. . . . . . . 8 ⊢ 𝑁 ⊆ suc 𝑁
7	6	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑁 ⊆ suc 𝑁)
8		eqid 2760	. . . . . . . . 9 ⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
9	8	satfsschain 36216	. . . . . . . 8 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)))
10	9	imp 412	. . . . . . 7 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) ∧ 𝑁 ⊆ suc 𝑁) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
11	2, 5, 7, 10	syl21anc 851	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))
12		eqid 2760	. . . . . . . 8 ⊢ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
13		eqid 2760	. . . . . . . 8 ⊢ {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}
14	8, 12, 13	satffunlem2lem1 36256	. . . . . . 7 ⊢ ((Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))})
15	14	expcom 419	. . . . . 6 ⊢ (((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}))
16	11, 15	syl 18	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}))
17	16	imp 412	. . . 4 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) → Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))})
18	8, 12, 13	satffunlem2lem2 36258	. . . 4 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) → (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∩ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}) = ∅)
19		funun 6587	. . . 4 ⊢ (((Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}) ∧ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∩ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}) = ∅) → Fun (((𝑀 Sat 𝐸)‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}))
20	1, 17, 18, 19	syl21anc 851	. . 3 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) → Fun (((𝑀 Sat 𝐸)‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}))
21		simpl 488	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 𝑀 ∈ 𝑉)
22		simpr 490	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 𝐸 ∈ 𝑊)
23		simpl 488	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑁 ∈ ω)
24	8, 12, 13	satfvsucsuc 36217	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → ((𝑀 Sat 𝐸)‘suc suc 𝑁) = (((𝑀 Sat 𝐸)‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}))
25	21, 22, 23, 24	syl2an23an 1450	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((𝑀 Sat 𝐸)‘suc suc 𝑁) = (((𝑀 Sat 𝐸)‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))}))
26	25	funeqd 6562	. . . 4 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁) ↔ Fun (((𝑀 Sat 𝐸)‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))})))
27	26	adantr 486	. . 3 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) → (Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁) ↔ Fun (((𝑀 Sat 𝐸)‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∨ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))})))
28	20, 27	mpbird 260	. 2 ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) → Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁))
29	28	ex 418	1 ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 {crab 3412 ⊆ wss 3895 ∖ cdif 4045 ∩ cin 4089 ∪ cun 4149 ∅c0 4278 {csn 4584 ⟨cop 4834 {copab 5166 dom cdm 5650 ↾ cres 5652 suc csuc 6364 Fun wfun 6533 ‘cfv 6539 (class class class)co 7421 ωcom 7878 1^st c1st 8000 2^nd c2nd 8001 ↑_m cmap 8851 ⊼_𝑔cgna 36186 ∀_𝑔cgol 36187 Sat csat 36188

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-map 8853 df-goel 36192 df-gona 36193 df-goal 36194 df-sat 36195 df-fmla 36197

This theorem is used by: satffun 36261

W3C validator