bnj153

Description: Technical lemma for bnj852 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj153.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj153.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj153.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj153.4	$⊢ θ \leftrightarrow ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land φ \land ψ))$
	bnj153.5	$⊢ τ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} θ)$
Assertion	bnj153	$⊢ n = 1_{𝑜} \to ((n \in D \land τ) \to θ)$

Proof

Step	Hyp	Ref	Expression
1		bnj153.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
2		bnj153.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj153.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj153.4	$⊢ θ \leftrightarrow ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land φ \land ψ))$
5		bnj153.5	$⊢ τ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} θ)$
6		biid	$⊢ ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
7		biid	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ$
8	1 7	bnj118	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
9	8	bicomi	$⊢ f (\emptyset) = pred (x, A, R) \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ$
10		bnj105	$⊢ 1_{𝑜} \in V$
11	2 10	bnj92	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ \leftrightarrow \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
12	11	bicomi	$⊢ \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ$
13		biid	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} θ$
14		biid	$⊢ ((R FrSe A \land x \in A) \to \exists f (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))) \leftrightarrow ((R FrSe A \land x \in A) \to \exists f (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))))$
15		biid	$⊢ ((R FrSe A \land x \in A) \to \exists^{} f (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))) \leftrightarrow ((R FrSe A \land x \in A) \to \exists^{} f (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))))$
16		biid	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
17		biid	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ$
18	6 16 7 17	bnj121	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ))$
19	8	anbi2i	$⊢ (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \leftrightarrow (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R))$
20	19 11	anbi12i	$⊢ ((f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow ((f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R)) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))$
21		df-3an	$⊢ (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow ((f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)$
22		df-3an	$⊢ (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))) \leftrightarrow ((f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R)) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))$
23	20 21 22	3bitr4i	$⊢ (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))$
24	23	imbi2i	$⊢ ((R FrSe A \land x \in A) \to (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))))$
25	18 24	bitri	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))))$
26	25	bicomi	$⊢ ((R FrSe A \land x \in A) \to (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))) \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
27		eqid	$⊢ \{⟨\emptyset, pred (x, A, R)⟩\} = \{⟨\emptyset, pred (x, A, R)⟩\}$
28		biid	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} f (\emptyset) = pred (x, A, R) \leftrightarrow \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} f (\emptyset) = pred (x, A, R)$
29		biid	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
30	26	sbcbii	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))) \leftrightarrow \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
31		biid	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ$
32		biid	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ$
33		biid	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
34	27 31 32 33 18	bnj124	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ))$
35	1 7 31 27	bnj125	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \leftrightarrow \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R)$
36	35	anbi2i	$⊢ (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \leftrightarrow (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R))$
37	2 17 32 27	bnj126	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ \leftrightarrow \forall i \in ω (suc i \in 1_{𝑜} \to \{⟨\emptyset, pred (x, A, R)⟩\} (suc i) = ⋃_{y \in \{⟨\emptyset, pred (x, A, R)⟩\} (i)} pred (y, A, R))$
38	36 37	anbi12i	$⊢ ((\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow ((\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R)) \land \forall i \in ω (suc i \in 1_{𝑜} \to \{⟨\emptyset, pred (x, A, R)⟩\} (suc i) = ⋃_{y \in \{⟨\emptyset, pred (x, A, R)⟩\} (i)} pred (y, A, R)))$
39		df-3an	$⊢ (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow ((\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)$
40		df-3an	$⊢ (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to \{⟨\emptyset, pred (x, A, R)⟩\} (suc i) = ⋃_{y \in \{⟨\emptyset, pred (x, A, R)⟩\} (i)} pred (y, A, R))) \leftrightarrow ((\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R)) \land \forall i \in ω (suc i \in 1_{𝑜} \to \{⟨\emptyset, pred (x, A, R)⟩\} (suc i) = ⋃_{y \in \{⟨\emptyset, pred (x, A, R)⟩\} (i)} pred (y, A, R)))$
41	38 39 40	3bitr4i	$⊢ (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to \{⟨\emptyset, pred (x, A, R)⟩\} (suc i) = ⋃_{y \in \{⟨\emptyset, pred (x, A, R)⟩\} (i)} pred (y, A, R)))$
42	41	imbi2i	$⊢ ((R FrSe A \land x \in A) \to (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to \{⟨\emptyset, pred (x, A, R)⟩\} (suc i) = ⋃_{y \in \{⟨\emptyset, pred (x, A, R)⟩\} (i)} pred (y, A, R))))$
43	34 42	bitri	$⊢ \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to \{⟨\emptyset, pred (x, A, R)⟩\} (suc i) = ⋃_{y \in \{⟨\emptyset, pred (x, A, R)⟩\} (i)} pred (y, A, R))))$
44	30 43	bitr2i	$⊢ ((R FrSe A \land x \in A) \to (\{⟨\emptyset, pred (x, A, R)⟩\} Fn 1_{𝑜} \land \{⟨\emptyset, pred (x, A, R)⟩\} (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to \{⟨\emptyset, pred (x, A, R)⟩\} (suc i) = ⋃_{y \in \{⟨\emptyset, pred (x, A, R)⟩\} (i)} pred (y, A, R)))) \leftrightarrow \underset{˙}{[} \{⟨\emptyset, pred (x, A, R)⟩\} / f \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))))$
45		biid	$⊢ (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))) \leftrightarrow (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))$
46		biid	$⊢ (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)$
47		biid	$⊢ \underset{˙}{[} g / f \underset{˙}{]} (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)$
48		biid	$⊢ \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ$
49		biid	$⊢ \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ$
50	46 47 48 49	bnj156	$⊢ \underset{˙}{[} g / f \underset{˙}{]} (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow (g Fn 1_{𝑜} \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)$
51	48 8	bnj154	$⊢ \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \leftrightarrow g (\emptyset) = pred (x, A, R)$
52	51	anbi2i	$⊢ (g Fn 1_{𝑜} \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \leftrightarrow (g Fn 1_{𝑜} \land g (\emptyset) = pred (x, A, R))$
53	17 11	bitri	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ \leftrightarrow \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
54	49 53	bnj155	$⊢ \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ \leftrightarrow \forall i \in ω (suc i \in 1_{𝑜} \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))$
55	52 54	anbi12i	$⊢ ((g Fn 1_{𝑜} \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow ((g Fn 1_{𝑜} \land g (\emptyset) = pred (x, A, R)) \land \forall i \in ω (suc i \in 1_{𝑜} \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))$
56		df-3an	$⊢ (g Fn 1_{𝑜} \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow ((g Fn 1_{𝑜} \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ) \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)$
57		df-3an	$⊢ (g Fn 1_{𝑜} \land g (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))) \leftrightarrow ((g Fn 1_{𝑜} \land g (\emptyset) = pred (x, A, R)) \land \forall i \in ω (suc i \in 1_{𝑜} \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))$
58	55 56 57	3bitr4i	$⊢ (g Fn 1_{𝑜} \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} g / f \underset{˙}{]} \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow (g Fn 1_{𝑜} \land g (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))$
59	50 58	bitri	$⊢ \underset{˙}{[} g / f \underset{˙}{]} (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow (g Fn 1_{𝑜} \land g (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R)))$
60	23	sbcbii	$⊢ \underset{˙}{[} g / f \underset{˙}{]} (f Fn 1_{𝑜} \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ) \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))$
61	59 60	bitr3i	$⊢ (g Fn 1_{𝑜} \land g (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to g (suc i) = ⋃_{y \in g (i)} pred (y, A, R))) \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} (f Fn 1_{𝑜} \land f (\emptyset) = pred (x, A, R) \land \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))$
62		biid	$⊢ \underset{˙}{[} g / f \underset{˙}{]} f (\emptyset) = pred (x, A, R) \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} f (\emptyset) = pred (x, A, R)$
63		biid	$⊢ \underset{˙}{[} g / f \underset{˙}{]} \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} \forall i \in ω (suc i \in 1_{𝑜} \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
64	1 2 3 4 5 6 9 12 13 14 15 26 27 28 29 44 45 61 62 63	bnj151	$⊢ n = 1_{𝑜} \to ((n \in D \land τ) \to θ)$

Metamath Proof Explorer

Theorem bnj153

Proof