Metamath Proof Explorer

Theorem satffunlem1

Description: Lemma 1 for satffun : induction basis. (Contributed by AV, 28-Oct-2023)

Ref Expression
Assertion satffunlem1 ⊢ M ∈ V ∧ E ∈ W → Fun ⁡ M Sat E ⁡ suc ⁡ ∅

Proof

Step Hyp Ref Expression
1 satfv0fun ⊢ M ∈ V ∧ E ∈ W → Fun ⁡ M Sat E ⁡ ∅
2 satffunlem1lem1 ⊢ Fun ⁡ M Sat E ⁡ ∅ → Fun ⁡ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u
3 1 2 syl ⊢ M ∈ V ∧ E ∈ W → Fun ⁡ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u
4 satffunlem1lem2 ⊢ M ∈ V ∧ E ∈ W → dom ⁡ M Sat E ⁡ ∅ ∩ dom ⁡ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u = ∅
5 funun ⊢ Fun ⁡ M Sat E ⁡ ∅ ∧ Fun ⁡ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u ∧ dom ⁡ M Sat E ⁡ ∅ ∩ dom ⁡ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u = ∅ → Fun ⁡ M Sat E ⁡ ∅ ∪ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u
6 1 3 4 5 syl21anc ⊢ M ∈ V ∧ E ∈ W → Fun ⁡ M Sat E ⁡ ∅ ∪ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u
7 peano1 ⊢ ∅ ∈ ω
8 eqid ⊢ M Sat E = M Sat E
9 8 satfvsuc ⊢ M ∈ V ∧ E ∈ W ∧ ∅ ∈ ω → M Sat E ⁡ suc ⁡ ∅ = M Sat E ⁡ ∅ ∪ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u
10 7 9 mp3an3 ⊢ M ∈ V ∧ E ∈ W → M Sat E ⁡ suc ⁡ ∅ = M Sat E ⁡ ∅ ∪ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u
11 10 funeqd ⊢ M ∈ V ∧ E ∈ W → Fun ⁡ M Sat E ⁡ suc ⁡ ∅ ↔ Fun ⁡ M Sat E ⁡ ∅ ∪ x y | ∃ u ∈ M Sat E ⁡ ∅ ∃ v ∈ M Sat E ⁡ ∅ x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = M ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = f ∈ M ω | ∀ j ∈ M i j ∪ f ↾ ω ∖ i ∈ 2 nd ⁡ u
12 6 11 mpbird ⊢ M ∈ V ∧ E ∈ W → Fun ⁡ M Sat E ⁡ suc ⁡ ∅