bnj580

Description: Technical lemma for bnj579 . 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	bnj580.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj580.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj580.3	$⊢ χ \leftrightarrow (f Fn n \land φ \land ψ)$
	bnj580.4	No typesetting found for \|- ( ph' <-> [. g / f ]. ph ) with typecode \|-
	bnj580.5	No typesetting found for \|- ( ps' <-> [. g / f ]. ps ) with typecode \|-
	bnj580.6	No typesetting found for \|- ( ch' <-> [. g / f ]. ch ) with typecode \|-
	bnj580.7	$⊢ D = ω ∖ \{\emptyset\}$
	bnj580.8	No typesetting found for \|- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
	bnj580.9	$⊢ τ \leftrightarrow \forall k \in n (k E j \to \underset{˙}{[} k / j \underset{˙}{]} θ)$
Assertion	bnj580	$⊢ n \in D \to \exists^{*} f χ$

Proof

Step	Hyp	Ref	Expression
1		bnj580.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
2		bnj580.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj580.3	$⊢ χ \leftrightarrow (f Fn n \land φ \land ψ)$
4		bnj580.4	Could not format ( ph' <-> [. g / f ]. ph ) : No typesetting found for \|- ( ph' <-> [. g / f ]. ph ) with typecode \|-
5		bnj580.5	Could not format ( ps' <-> [. g / f ]. ps ) : No typesetting found for \|- ( ps' <-> [. g / f ]. ps ) with typecode \|-
6		bnj580.6	Could not format ( ch' <-> [. g / f ]. ch ) : No typesetting found for \|- ( ch' <-> [. g / f ]. ch ) with typecode \|-
7		bnj580.7	$⊢ D = ω ∖ \{\emptyset\}$
8		bnj580.8	Could not format ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
9		bnj580.9	$⊢ τ \leftrightarrow \forall k \in n (k E j \to \underset{˙}{[} k / j \underset{˙}{]} θ)$
10	3	simp1bi	$⊢ χ \to f Fn n$
11	3 4 5 6	bnj581	Could not format ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) with typecode \|-
12	11	simp1bi	Could not format ( ch' -> g Fn n ) : No typesetting found for \|- ( ch' -> g Fn n ) with typecode \|-
13	10 12	bnj240	Could not format ( ( n e. D /\ ch /\ ch' ) -> ( f Fn n /\ g Fn n ) ) : No typesetting found for \|- ( ( n e. D /\ ch /\ ch' ) -> ( f Fn n /\ g Fn n ) ) with typecode \|-
14	4 1	bnj154	Could not format ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
15		vex	$⊢ g \in V$
16	2 5 15	bnj540	Could not format ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode \|-
17	8	bnj591	Could not format ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) : No typesetting found for \|- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) with typecode \|-
18	1 2 3 7 14 16 11 8 17 9	bnj594	$⊢ (j \in n \land τ) \to θ$
19	18	ex	$⊢ j \in n \to (τ \to θ)$
20	19	rgen	$⊢ \forall j \in n (τ \to θ)$
21		vex	$⊢ n \in V$
22	21 9	bnj110	$⊢ (E Fr n \land \forall j \in n (τ \to θ)) \to \forall j \in n θ$
23	20 22	mpan2	$⊢ E Fr n \to \forall j \in n θ$
24	8	ralbii	Could not format ( A. j e. n th <-> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( A. j e. n th <-> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
25	23 24	sylib	Could not format ( _E Fr n -> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( _E Fr n -> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
26	25	r19.21be	Could not format A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
27	7	bnj923	$⊢ n \in D \to n \in ω$
28		nnord	$⊢ n \in ω \to Ord n$
29		ordfr	$⊢ Ord n \to E Fr n$
30	27 28 29	3syl	$⊢ n \in D \to E Fr n$
31	30	3ad2ant1	Could not format ( ( n e. D /\ ch /\ ch' ) -> _E Fr n ) : No typesetting found for \|- ( ( n e. D /\ ch /\ ch' ) -> _E Fr n ) with typecode \|-
32	31	pm4.71ri	Could not format ( ( n e. D /\ ch /\ ch' ) <-> ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) ) : No typesetting found for \|- ( ( n e. D /\ ch /\ ch' ) <-> ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) ) with typecode \|-
33	32	imbi1i	Could not format ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
34		impexp	Could not format ( ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) : No typesetting found for \|- ( ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) with typecode \|-
35	33 34	bitri	Could not format ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) : No typesetting found for \|- ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) with typecode \|-
36	35	ralbii	Could not format ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) : No typesetting found for \|- ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) with typecode \|-
37	26 36	mpbir	Could not format A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) : No typesetting found for \|- A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) with typecode \|-
38		r19.21v	Could not format ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) ) with typecode \|-
39	37 38	mpbi	Could not format ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) : No typesetting found for \|- ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) with typecode \|-
40		eqfnfv	$⊢ (f Fn n \land g Fn n) \to (f = g \leftrightarrow \forall j \in n f (j) = g (j))$
41	40	biimprd	$⊢ (f Fn n \land g Fn n) \to (\forall j \in n f (j) = g (j) \to f = g)$
42	13 39 41	sylc	Could not format ( ( n e. D /\ ch /\ ch' ) -> f = g ) : No typesetting found for \|- ( ( n e. D /\ ch /\ ch' ) -> f = g ) with typecode \|-
43	42	3expib	Could not format ( n e. D -> ( ( ch /\ ch' ) -> f = g ) ) : No typesetting found for \|- ( n e. D -> ( ( ch /\ ch' ) -> f = g ) ) with typecode \|-
44	43	alrimivv	Could not format ( n e. D -> A. f A. g ( ( ch /\ ch' ) -> f = g ) ) : No typesetting found for \|- ( n e. D -> A. f A. g ( ( ch /\ ch' ) -> f = g ) ) with typecode \|-
45		sbsbc	$⊢ [g/ f] χ \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} χ$
46	45	anbi2i	$⊢ (χ \land [g/ f] χ) \leftrightarrow (χ \land \underset{˙}{[} g / f \underset{˙}{]} χ)$
47	46	imbi1i	$⊢ ((χ \land [g/ f] χ) \to f = g) \leftrightarrow ((χ \land \underset{˙}{[} g / f \underset{˙}{]} χ) \to f = g)$
48	47	2albii	$⊢ \forall f \forall g ((χ \land [g/ f] χ) \to f = g) \leftrightarrow \forall f \forall g ((χ \land \underset{˙}{[} g / f \underset{˙}{]} χ) \to f = g)$
49		nfv	$⊢ Ⅎ g χ$
50	49	mo3	$⊢ \exists^{*} f χ \leftrightarrow \forall f \forall g ((χ \land [g/ f] χ) \to f = g)$
51	6	anbi2i	Could not format ( ( ch /\ ch' ) <-> ( ch /\ [. g / f ]. ch ) ) : No typesetting found for \|- ( ( ch /\ ch' ) <-> ( ch /\ [. g / f ]. ch ) ) with typecode \|-
52	51	imbi1i	Could not format ( ( ( ch /\ ch' ) -> f = g ) <-> ( ( ch /\ [. g / f ]. ch ) -> f = g ) ) : No typesetting found for \|- ( ( ( ch /\ ch' ) -> f = g ) <-> ( ( ch /\ [. g / f ]. ch ) -> f = g ) ) with typecode \|-
53	52	2albii	Could not format ( A. f A. g ( ( ch /\ ch' ) -> f = g ) <-> A. f A. g ( ( ch /\ [. g / f ]. ch ) -> f = g ) ) : No typesetting found for \|- ( A. f A. g ( ( ch /\ ch' ) -> f = g ) <-> A. f A. g ( ( ch /\ [. g / f ]. ch ) -> f = g ) ) with typecode \|-
54	48 50 53	3bitr4i	Could not format ( E* f ch <-> A. f A. g ( ( ch /\ ch' ) -> f = g ) ) : No typesetting found for \|- ( E* f ch <-> A. f A. g ( ( ch /\ ch' ) -> f = g ) ) with typecode \|-
55	44 54	sylibr	$⊢ n \in D \to \exists^{*} f χ$

Metamath Proof Explorer

Theorem bnj580

Proof