satfv1lem

		Ref	Expression
	Assertion	satfv1lem	$⊢ (N \in ω \land I \in ω \land J \in ω) \to \{a \in (M^{ω}) \| \forall z \in M \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in \{b \in (M^{ω}) \| b (I) E b (J)\}\} = \{a \in (M^{ω}) \| \forall z \in M if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J)))\}$

Proof

Step	Hyp	Ref	Expression
1		fveq1	$⊢ b = \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \to b (I) = (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I)$
2		fveq1	$⊢ b = \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \to b (J) = (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J)$
3	1 2	breq12d	$⊢ b = \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \to (b (I) E b (J) \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J))$
4	3	elrab	$⊢ \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in \{b \in (M^{ω}) \| b (I) E b (J)\} \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}) \land (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J))$
5	4	a1i	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in \{b \in (M^{ω}) \| b (I) E b (J)\} \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}) \land (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J)))$
6		elex	$⊢ N \in ω \to N \in V$
7	6	3ad2ant1	$⊢ (N \in ω \land I \in ω \land J \in ω) \to N \in V$
8	7	ad2antrr	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to N \in V$
9		simpr	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to z \in M$
10	8 9	fsnd	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to \{⟨N, z⟩\} : \{N\} ⟶ M$
11		elmapex	$⊢ a \in (M^{ω}) \to (M \in V \land ω \in V)$
12	11	simpld	$⊢ a \in (M^{ω}) \to M \in V$
13	12	adantr	$⊢ (a \in (M^{ω}) \land z \in M) \to M \in V$
14		snex	$⊢ \{N\} \in V$
15	14	a1i	$⊢ (a \in (M^{ω}) \land z \in M) \to \{N\} \in V$
16	13 15	elmapd	$⊢ (a \in (M^{ω}) \land z \in M) \to (\{⟨N, z⟩\} \in (M^{\{N\}}) \leftrightarrow \{⟨N, z⟩\} : \{N\} ⟶ M)$
17	16	adantll	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to (\{⟨N, z⟩\} \in (M^{\{N\}}) \leftrightarrow \{⟨N, z⟩\} : \{N\} ⟶ M)$
18	10 17	mpbird	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to \{⟨N, z⟩\} \in (M^{\{N\}})$
19		elmapi	$⊢ a \in (M^{ω}) \to a : ω ⟶ M$
20		difssd	$⊢ a \in (M^{ω}) \to ω ∖ \{N\} \subseteq ω$
21	19 20	fssresd	$⊢ a \in (M^{ω}) \to ({a ↾}_{(ω ∖ \{N\})}) : ω ∖ \{N\} ⟶ M$
22		omex	$⊢ ω \in V$
23	22	difexi	$⊢ ω ∖ \{N\} \in V$
24	23	a1i	$⊢ a \in (M^{ω}) \to ω ∖ \{N\} \in V$
25	12 24	elmapd	$⊢ a \in (M^{ω}) \to ({a ↾}_{(ω ∖ \{N\})} \in (M^{(ω ∖ \{N\})}) \leftrightarrow ({a ↾}_{(ω ∖ \{N\})}) : ω ∖ \{N\} ⟶ M)$
26	21 25	mpbird	$⊢ a \in (M^{ω}) \to {a ↾}_{(ω ∖ \{N\})} \in (M^{(ω ∖ \{N\})})$
27	26	adantl	$⊢ ((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \to {a ↾}_{(ω ∖ \{N\})} \in (M^{(ω ∖ \{N\})})$
28	27	adantr	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to {a ↾}_{(ω ∖ \{N\})} \in (M^{(ω ∖ \{N\})})$
29		res0	$⊢ {\{⟨N, z⟩\} ↾}_{\emptyset} = \emptyset$
30		res0	$⊢ {({a ↾}_{(ω ∖ \{N\})}) ↾}_{\emptyset} = \emptyset$
31	29 30	eqtr4i	$⊢ {\{⟨N, z⟩\} ↾}_{\emptyset} = {({a ↾}_{(ω ∖ \{N\})}) ↾}_{\emptyset}$
32		disjdif	$⊢ \{N\} \cap (ω ∖ \{N\}) = \emptyset$
33	32	reseq2i	$⊢ {\{⟨N, z⟩\} ↾}_{(\{N\} \cap (ω ∖ \{N\}))} = {\{⟨N, z⟩\} ↾}_{\emptyset}$
34	32	reseq2i	$⊢ {({a ↾}_{(ω ∖ \{N\})}) ↾}_{(\{N\} \cap (ω ∖ \{N\}))} = {({a ↾}_{(ω ∖ \{N\})}) ↾}_{\emptyset}$
35	31 33 34	3eqtr4i	$⊢ {\{⟨N, z⟩\} ↾}_{(\{N\} \cap (ω ∖ \{N\}))} = {({a ↾}_{(ω ∖ \{N\})}) ↾}_{(\{N\} \cap (ω ∖ \{N\}))}$
36	35	a1i	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to {\{⟨N, z⟩\} ↾}_{(\{N\} \cap (ω ∖ \{N\}))} = {({a ↾}_{(ω ∖ \{N\})}) ↾}_{(\{N\} \cap (ω ∖ \{N\}))}$
37		elmapresaun	$⊢ (\{⟨N, z⟩\} \in (M^{\{N\}}) \land {a ↾}_{(ω ∖ \{N\})} \in (M^{(ω ∖ \{N\})}) \land {\{⟨N, z⟩\} ↾}_{(\{N\} \cap (ω ∖ \{N\}))} = {({a ↾}_{(ω ∖ \{N\})}) ↾}_{(\{N\} \cap (ω ∖ \{N\}))}) \to \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{(\{N\} \cup (ω ∖ \{N\}))})$
38	18 28 36 37	syl3anc	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{(\{N\} \cup (ω ∖ \{N\}))})$
39		uncom	$⊢ \{N\} \cup (ω ∖ \{N\}) = (ω ∖ \{N\}) \cup \{N\}$
40		difsnid	$⊢ N \in ω \to (ω ∖ \{N\}) \cup \{N\} = ω$
41	39 40	syl5req	$⊢ N \in ω \to ω = \{N\} \cup (ω ∖ \{N\})$
42	41	3ad2ant1	$⊢ (N \in ω \land I \in ω \land J \in ω) \to ω = \{N\} \cup (ω ∖ \{N\})$
43	42	ad2antrr	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to ω = \{N\} \cup (ω ∖ \{N\})$
44	43	oveq2d	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to M^{ω} = M^{(\{N\} \cup (ω ∖ \{N\}))}$
45	38 44	eleqtrrd	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})$
46		ibar	$⊢ \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}) \land (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J)))$
47	46	adantl	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}) \land (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J)))$
48	47	bicomd	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}) \land (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J)) \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J))$
49		simpll1	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to N \in ω$
50		eqid	$⊢ \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) = \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})$
51	49 9 50	fvsnun1	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) = z$
52	51	adantr	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) = z$
53	52 52	breq12d	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) \leftrightarrow z E z)$
54	53	adantl	$⊢ (J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) \leftrightarrow z E z)$
55		fveq2	$⊢ J = N \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) = (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N)$
56	55	breq2d	$⊢ J = N \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N))$
57		ifptru	$⊢ J = N \to (if- (J = N, z E z, z E a (J)) \leftrightarrow z E z)$
58	56 57	bibi12d	$⊢ J = N \to (((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, z E z, z E a (J))) \leftrightarrow ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) \leftrightarrow z E z))$
59	58	adantr	$⊢ (J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, z E z, z E a (J))) \leftrightarrow ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) \leftrightarrow z E z))$
60	54 59	mpbird	$⊢ (J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, z E z, z E a (J)))$
61	52	adantl	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) = z$
62	49	adantr	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to N \in ω$
63	62	adantl	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to N \in ω$
64	9	adantr	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to z \in M$
65	64	adantl	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to z \in M$
66		neqne	$⊢ \neg J = N \to J \neq N$
67		simpll3	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to J \in ω$
68	67	adantr	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to J \in ω$
69	66 68	anim12ci	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (J \in ω \land J \neq N)$
70		eldifsn	$⊢ J \in (ω ∖ \{N\}) \leftrightarrow (J \in ω \land J \neq N)$
71	69 70	sylibr	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to J \in (ω ∖ \{N\})$
72	63 65 50 71	fvsnun2	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) = a (J)$
73	61 72	breq12d	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow z E a (J))$
74		ifpfal	$⊢ \neg J = N \to (if- (J = N, z E z, z E a (J)) \leftrightarrow z E a (J))$
75	74	bicomd	$⊢ \neg J = N \to (z E a (J) \leftrightarrow if- (J = N, z E z, z E a (J)))$
76	75	adantr	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (z E a (J) \leftrightarrow if- (J = N, z E z, z E a (J)))$
77	73 76	bitrd	$⊢ (\neg J = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, z E z, z E a (J)))$
78	60 77	pm2.61ian	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, z E z, z E a (J)))$
79	78	adantl	$⊢ (I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, z E z, z E a (J)))$
80		fveq2	$⊢ I = N \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) = (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N)$
81	80	breq1d	$⊢ I = N \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J))$
82		ifptru	$⊢ I = N \to (if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))) \leftrightarrow if- (J = N, z E z, z E a (J)))$
83	81 82	bibi12d	$⊢ I = N \to (((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J)))) \leftrightarrow ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, z E z, z E a (J))))$
84	83	adantr	$⊢ (I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J)))) \leftrightarrow ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, z E z, z E a (J))))$
85	79 84	mpbird	$⊢ (I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
86	62	adantl	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to N \in ω$
87	64	adantl	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to z \in M$
88		neqne	$⊢ \neg I = N \to I \neq N$
89		simpll2	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to I \in ω$
90	89	adantr	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to I \in ω$
91	88 90	anim12ci	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (I \in ω \land I \neq N)$
92		eldifsn	$⊢ I \in (ω ∖ \{N\}) \leftrightarrow (I \in ω \land I \neq N)$
93	91 92	sylibr	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to I \in (ω ∖ \{N\})$
94	86 87 50 93	fvsnun2	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) = a (I)$
95	52	adantl	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) = z$
96	94 95	breq12d	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) \leftrightarrow a (I) E z)$
97	96	adantl	$⊢ (J = N \land (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) \leftrightarrow a (I) E z)$
98	55	breq2d	$⊢ J = N \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N))$
99		ifptru	$⊢ J = N \to (if- (J = N, a (I) E z, a (I) E a (J)) \leftrightarrow a (I) E z)$
100	98 99	bibi12d	$⊢ J = N \to (((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, a (I) E z, a (I) E a (J))) \leftrightarrow ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) \leftrightarrow a (I) E z))$
101	100	adantr	$⊢ (J = N \land (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})))) \to (((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, a (I) E z, a (I) E a (J))) \leftrightarrow ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (N) \leftrightarrow a (I) E z))$
102	97 101	mpbird	$⊢ (J = N \land (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, a (I) E z, a (I) E a (J)))$
103	94	adantl	$⊢ (\neg J = N \land (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})))) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) = a (I)$
104	72	adantrl	$⊢ (\neg J = N \land (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})))) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) = a (J)$
105	103 104	breq12d	$⊢ (\neg J = N \land (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow a (I) E a (J))$
106		ifpfal	$⊢ \neg J = N \to (if- (J = N, a (I) E z, a (I) E a (J)) \leftrightarrow a (I) E a (J))$
107	106	bicomd	$⊢ \neg J = N \to (a (I) E a (J) \leftrightarrow if- (J = N, a (I) E z, a (I) E a (J)))$
108	107	adantr	$⊢ (\neg J = N \land (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})))) \to (a (I) E a (J) \leftrightarrow if- (J = N, a (I) E z, a (I) E a (J)))$
109	105 108	bitrd	$⊢ (\neg J = N \land (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, a (I) E z, a (I) E a (J)))$
110	102 109	pm2.61ian	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (J = N, a (I) E z, a (I) E a (J)))$
111		ifpfal	$⊢ \neg I = N \to (if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))) \leftrightarrow if- (J = N, a (I) E z, a (I) E a (J)))$
112	111	bicomd	$⊢ \neg I = N \to (if- (J = N, a (I) E z, a (I) E a (J)) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
113	112	adantr	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to (if- (J = N, a (I) E z, a (I) E a (J)) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
114	110 113	bitrd	$⊢ (\neg I = N \land ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}))) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
115	85 114	pm2.61ian	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
116	48 115	bitrd	$⊢ ((((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \land \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω})) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}) \land (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J)) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
117	45 116	mpdan	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to ((\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in (M^{ω}) \land (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (I) E (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})})) (J)) \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
118	5 117	bitrd	$⊢ (((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \land z \in M) \to (\{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in \{b \in (M^{ω}) \| b (I) E b (J)\} \leftrightarrow if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
119	118	ralbidva	$⊢ ((N \in ω \land I \in ω \land J \in ω) \land a \in (M^{ω})) \to (\forall z \in M \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in \{b \in (M^{ω}) \| b (I) E b (J)\} \leftrightarrow \forall z \in M if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J))))$
120	119	rabbidva	$⊢ (N \in ω \land I \in ω \land J \in ω) \to \{a \in (M^{ω}) \| \forall z \in M \{⟨N, z⟩\} \cup ({a ↾}_{(ω ∖ \{N\})}) \in \{b \in (M^{ω}) \| b (I) E b (J)\}\} = \{a \in (M^{ω}) \| \forall z \in M if- (I = N, if- (J = N, z E z, z E a (J)), if- (J = N, a (I) E z, a (I) E a (J)))\}$

Metamath Proof Explorer

Theorem satfv1lem

Proof