bnj1128

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

Proof

Step	Hyp	Ref	Expression
1		bnj1128.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1128.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1128.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj1128.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		bnj1128.5	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
6		bnj1128.6	$⊢ θ \leftrightarrow (χ \to f (i) \subseteq A)$
7		bnj1128.7	$⊢ τ \leftrightarrow \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} θ)$
8		bnj1128.8	Could not format ( ph' <-> [. j / i ]. ph ) : No typesetting found for \|- ( ph' <-> [. j / i ]. ph ) with typecode \|-
9		bnj1128.9	Could not format ( ps' <-> [. j / i ]. ps ) : No typesetting found for \|- ( ps' <-> [. j / i ]. ps ) with typecode \|-
10		bnj1128.10	Could not format ( ch' <-> [. j / i ]. ch ) : No typesetting found for \|- ( ch' <-> [. j / i ]. ch ) with typecode \|-
11		bnj1128.11	Could not format ( th' <-> [. j / i ]. th ) : No typesetting found for \|- ( th' <-> [. j / i ]. th ) with typecode \|-
12	1 2 3 4 5	bnj981	$⊢ Y \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land Y \in f (i))$
13		simp1	$⊢ (χ \land i \in n \land Y \in f (i)) \to χ$
14		simp2	$⊢ (χ \land i \in n \land Y \in f (i)) \to i \in n$
15		nfv	$⊢ Ⅎ j i \in n$
16		nfra1	$⊢ Ⅎ j \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} θ)$
17	7 16	nfxfr	$⊢ Ⅎ j τ$
18		nfv	$⊢ Ⅎ j χ$
19	15 17 18	nf3an	$⊢ Ⅎ j (i \in n \land τ \land χ)$
20		nfv	$⊢ Ⅎ j f (i) \subseteq A$
21	19 20	nfim	$⊢ Ⅎ j ((i \in n \land τ \land χ) \to f (i) \subseteq A)$
22	21	nf5ri	$⊢ ((i \in n \land τ \land χ) \to f (i) \subseteq A) \to \forall j ((i \in n \land τ \land χ) \to f (i) \subseteq A)$
23	3	bnj1098	$⊢ \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in n \land i = suc j))$
24		simpl	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ)) \to i \neq \emptyset$
25		simpr1	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ)) \to i \in n$
26	5	bnj1232	$⊢ χ \to n \in D$
27	26	3ad2ant3	$⊢ (i \in n \land τ \land χ) \to n \in D$
28	27	adantl	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ)) \to n \in D$
29	24 25 28	3jca	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ)) \to (i \neq \emptyset \land i \in n \land n \in D)$
30	23 29	bnj1101	$⊢ \exists j ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to (j \in n \land i = suc j))$
31		ancl	$⊢ ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to (j \in n \land i = suc j)) \to ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to ((i \neq \emptyset \land (i \in n \land τ \land χ)) \land (j \in n \land i = suc j)))$
32	30 31	bnj101	$⊢ \exists j ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to ((i \neq \emptyset \land (i \in n \land τ \land χ)) \land (j \in n \land i = suc j)))$
33		df-3an	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \leftrightarrow ((i \neq \emptyset \land (i \in n \land τ \land χ)) \land (j \in n \land i = suc j))$
34	33	imbi2i	$⊢ ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j))) \leftrightarrow ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to ((i \neq \emptyset \land (i \in n \land τ \land χ)) \land (j \in n \land i = suc j)))$
35	34	exbii	$⊢ \exists j ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j))) \leftrightarrow \exists j ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to ((i \neq \emptyset \land (i \in n \land τ \land χ)) \land (j \in n \land i = suc j)))$
36	32 35	mpbir	$⊢ \exists j ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)))$
37		bnj213	$⊢ pred (y, A, R) \subseteq A$
38	37	bnj226	$⊢ ⋃_{y \in f (j)} pred (y, A, R) \subseteq A$
39		simp21	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \to i \in n$
40		simp3r	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \to i = suc j$
41		biid	$⊢ n \in D \leftrightarrow n \in D$
42		biid	$⊢ f Fn n \leftrightarrow f Fn n$
43		vex	$⊢ j \in V$
44		sbcg	$⊢ j \in V \to (\underset{˙}{[} j / i \underset{˙}{]} φ \leftrightarrow φ)$
45	43 44	ax-mp	$⊢ \underset{˙}{[} j / i \underset{˙}{]} φ \leftrightarrow φ$
46	8 45	bitr2i	Could not format ( ph <-> ph' ) : No typesetting found for \|- ( ph <-> ph' ) with typecode \|-
47	2 9	bnj1039	Could not format ( ps' <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
48	2 47	bitr4i	Could not format ( ps <-> ps' ) : No typesetting found for \|- ( ps <-> ps' ) with typecode \|-
49	41 42 46 48	bnj887	Could not format ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode \|-
50	8 9 5 10	bnj1040	Could not format ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode \|-
51	49 5 50	3bitr4i	Could not format ( ch <-> ch' ) : No typesetting found for \|- ( ch <-> ch' ) with typecode \|-
52	50	bnj1254	Could not format ( ch' -> ps' ) : No typesetting found for \|- ( ch' -> ps' ) with typecode \|-
53	51 52	sylbi	Could not format ( ch -> ps' ) : No typesetting found for \|- ( ch -> ps' ) with typecode \|-
54	53	3ad2ant3	Could not format ( ( i e. n /\ ta /\ ch ) -> ps' ) : No typesetting found for \|- ( ( i e. n /\ ta /\ ch ) -> ps' ) with typecode \|-
55	54	3ad2ant2	Could not format ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ps' ) : No typesetting found for \|- ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ps' ) with typecode \|-
56		simp3l	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \to j \in n$
57	27	3ad2ant2	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \to n \in D$
58	3	bnj923	$⊢ n \in D \to n \in ω$
59		elnn	$⊢ (j \in n \land n \in ω) \to j \in ω$
60	58 59	sylan2	$⊢ (j \in n \land n \in D) \to j \in ω$
61	56 57 60	syl2anc	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \to j \in ω$
62	47	bnj589	Could not format ( ps' <-> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) with typecode \|-
63		rsp	$⊢ \forall j \in ω (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)) \to (j \in ω \to (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)))$
64	62 63	sylbi	Could not format ( ps' -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) : No typesetting found for \|- ( ps' -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) with typecode \|-
65		eleq1	$⊢ i = suc j \to (i \in n \leftrightarrow suc j \in n)$
66		fveqeq2	$⊢ i = suc j \to (f (i) = ⋃_{y \in f (j)} pred (y, A, R) \leftrightarrow f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
67	65 66	imbi12d	$⊢ i = suc j \to ((i \in n \to f (i) = ⋃_{y \in f (j)} pred (y, A, R)) \leftrightarrow (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)))$
68	67	imbi2d	$⊢ i = suc j \to ((j \in ω \to (i \in n \to f (i) = ⋃_{y \in f (j)} pred (y, A, R))) \leftrightarrow (j \in ω \to (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))))$
69	64 68	syl5ibr	Could not format ( i = suc j -> ( ps' -> ( j e. _om -> ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) ) : No typesetting found for \|- ( i = suc j -> ( ps' -> ( j e. _om -> ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) ) with typecode \|-
70	40 55 61 69	syl3c	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \to (i \in n \to f (i) = ⋃_{y \in f (j)} pred (y, A, R))$
71	39 70	mpd	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \to f (i) = ⋃_{y \in f (j)} pred (y, A, R)$
72	38 71	bnj1262	$⊢ (i \neq \emptyset \land (i \in n \land τ \land χ) \land (j \in n \land i = suc j)) \to f (i) \subseteq A$
73	36 72	bnj1023	$⊢ \exists j ((i \neq \emptyset \land (i \in n \land τ \land χ)) \to f (i) \subseteq A)$
74	5	bnj1247	$⊢ χ \to φ$
75	74	3ad2ant3	$⊢ (i \in n \land τ \land χ) \to φ$
76		bnj213	$⊢ pred (X, A, R) \subseteq A$
77		fveq2	$⊢ i = \emptyset \to f (i) = f (\emptyset)$
78	1	biimpi	$⊢ φ \to f (\emptyset) = pred (X, A, R)$
79	77 78	sylan9eq	$⊢ (i = \emptyset \land φ) \to f (i) = pred (X, A, R)$
80	76 79	bnj1262	$⊢ (i = \emptyset \land φ) \to f (i) \subseteq A$
81	75 80	sylan2	$⊢ (i = \emptyset \land (i \in n \land τ \land χ)) \to f (i) \subseteq A$
82	73 81	bnj1109	$⊢ \exists j ((i \in n \land τ \land χ) \to f (i) \subseteq A)$
83	22 82	bnj1131	$⊢ (i \in n \land τ \land χ) \to f (i) \subseteq A$
84	83	3expia	$⊢ (i \in n \land τ) \to (χ \to f (i) \subseteq A)$
85	84 6	sylibr	$⊢ (i \in n \land τ) \to θ$
86	3 5 7 85	bnj1133	$⊢ χ \to \forall i \in n θ$
87	6	ralbii	$⊢ \forall i \in n θ \leftrightarrow \forall i \in n (χ \to f (i) \subseteq A)$
88	86 87	sylib	$⊢ χ \to \forall i \in n (χ \to f (i) \subseteq A)$
89		rsp	$⊢ \forall i \in n (χ \to f (i) \subseteq A) \to (i \in n \to (χ \to f (i) \subseteq A))$
90	88 89	syl	$⊢ χ \to (i \in n \to (χ \to f (i) \subseteq A))$
91	13 14 13 90	syl3c	$⊢ (χ \land i \in n \land Y \in f (i)) \to f (i) \subseteq A$
92		simp3	$⊢ (χ \land i \in n \land Y \in f (i)) \to Y \in f (i)$
93	91 92	sseldd	$⊢ (χ \land i \in n \land Y \in f (i)) \to Y \in A$
94	93	2eximi	$⊢ \exists n \exists i (χ \land i \in n \land Y \in f (i)) \to \exists n \exists i Y \in A$
95	12 94	bnj593	$⊢ Y \in trCl (X, A, R) \to \exists f \exists n \exists i Y \in A$
96		19.9v	$⊢ \exists f \exists n \exists i Y \in A \leftrightarrow \exists n \exists i Y \in A$
97		19.9v	$⊢ \exists n \exists i Y \in A \leftrightarrow \exists i Y \in A$
98		19.9v	$⊢ \exists i Y \in A \leftrightarrow Y \in A$
99	96 97 98	3bitri	$⊢ \exists f \exists n \exists i Y \in A \leftrightarrow Y \in A$
100	95 99	sylib	$⊢ Y \in trCl (X, A, R) \to Y \in A$

Metamath Proof Explorer

Theorem bnj1128

Proof