bnj1145

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	bnj1145.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj1145.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj1145.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj1145.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj1145.5	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1145.6	$⊢ θ \leftrightarrow ((i \neq \emptyset \land i \in n \land χ) \land (j \in n \land i = suc j))$
Assertion	bnj1145	$⊢ trCl (X, A, R) \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		bnj1145.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1145.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1145.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj1145.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		bnj1145.5	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
6		bnj1145.6	$⊢ θ \leftrightarrow ((i \neq \emptyset \land i \in n \land χ) \land (j \in n \land i = suc j))$
7	1 2 3 4	bnj882	$⊢ trCl (X, A, R) = ⋃_{f \in B} ⋃_{i \in dom f} f (i)$
8		ss2iun	$⊢ \forall f \in B ⋃_{i \in dom f} f (i) \subseteq A \to ⋃_{f \in B} ⋃_{i \in dom f} f (i) \subseteq ⋃_{f \in B} A$
9	5 4	bnj1083	$⊢ f \in B \leftrightarrow \exists n χ$
10	2	bnj1095	$⊢ ψ \to \forall i ψ$
11	10 5	bnj1096	$⊢ χ \to \forall i χ$
12	3	bnj1098	$⊢ \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in n \land i = suc j))$
13	5	bnj1232	$⊢ χ \to n \in D$
14	13	3anim3i	$⊢ (i \neq \emptyset \land i \in n \land χ) \to (i \neq \emptyset \land i \in n \land n \in D)$
15	12 14	bnj1101	$⊢ \exists j ((i \neq \emptyset \land i \in n \land χ) \to (j \in n \land i = suc j))$
16		ancl	$⊢ ((i \neq \emptyset \land i \in n \land χ) \to (j \in n \land i = suc j)) \to ((i \neq \emptyset \land i \in n \land χ) \to ((i \neq \emptyset \land i \in n \land χ) \land (j \in n \land i = suc j)))$
17	15 16	bnj101	$⊢ \exists j ((i \neq \emptyset \land i \in n \land χ) \to ((i \neq \emptyset \land i \in n \land χ) \land (j \in n \land i = suc j)))$
18	6	imbi2i	$⊢ ((i \neq \emptyset \land i \in n \land χ) \to θ) \leftrightarrow ((i \neq \emptyset \land i \in n \land χ) \to ((i \neq \emptyset \land i \in n \land χ) \land (j \in n \land i = suc j)))$
19	18	exbii	$⊢ \exists j ((i \neq \emptyset \land i \in n \land χ) \to θ) \leftrightarrow \exists j ((i \neq \emptyset \land i \in n \land χ) \to ((i \neq \emptyset \land i \in n \land χ) \land (j \in n \land i = suc j)))$
20	17 19	mpbir	$⊢ \exists j ((i \neq \emptyset \land i \in n \land χ) \to θ)$
21		bnj213	$⊢ pred (y, A, R) \subseteq A$
22	21	bnj226	$⊢ ⋃_{y \in f (j)} pred (y, A, R) \subseteq A$
23		simpr	$⊢ (j \in n \land i = suc j) \to i = suc j$
24	6 23	simplbiim	$⊢ θ \to i = suc j$
25		simp2	$⊢ (i \neq \emptyset \land i \in n \land χ) \to i \in n$
26	13	3ad2ant3	$⊢ (i \neq \emptyset \land i \in n \land χ) \to n \in D$
27	3	bnj923	$⊢ n \in D \to n \in ω$
28		elnn	$⊢ (i \in n \land n \in ω) \to i \in ω$
29	27 28	sylan2	$⊢ (i \in n \land n \in D) \to i \in ω$
30	25 26 29	syl2anc	$⊢ (i \neq \emptyset \land i \in n \land χ) \to i \in ω$
31	6 30	bnj832	$⊢ θ \to i \in ω$
32		vex	$⊢ j \in V$
33	32	bnj216	$⊢ i = suc j \to j \in i$
34		elnn	$⊢ (j \in i \land i \in ω) \to j \in ω$
35	33 34	sylan	$⊢ (i = suc j \land i \in ω) \to j \in ω$
36	24 31 35	syl2anc	$⊢ θ \to j \in ω$
37	6 25	bnj832	$⊢ θ \to i \in n$
38	24 37	eqeltrrd	$⊢ θ \to suc j \in n$
39	2	bnj589	$⊢ ψ \leftrightarrow \forall j \in ω (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
40	39	biimpi	$⊢ ψ \to \forall j \in ω (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
41	40	bnj708	$⊢ (n \in D \land f Fn n \land φ \land ψ) \to \forall j \in ω (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
42		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)))$
43	41 42	syl	$⊢ (n \in D \land f Fn n \land φ \land ψ) \to (j \in ω \to (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)))$
44	5 43	sylbi	$⊢ χ \to (j \in ω \to (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)))$
45	44	3ad2ant3	$⊢ (i \neq \emptyset \land i \in n \land χ) \to (j \in ω \to (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)))$
46	6 45	bnj832	$⊢ θ \to (j \in ω \to (suc j \in n \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)))$
47	36 38 46	mp2d	$⊢ θ \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)$
48		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))$
49	24 48	syl	$⊢ θ \to (f (i) = ⋃_{y \in f (j)} pred (y, A, R) \leftrightarrow f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
50	47 49	mpbird	$⊢ θ \to f (i) = ⋃_{y \in f (j)} pred (y, A, R)$
51	22 50	bnj1262	$⊢ θ \to f (i) \subseteq A$
52	20 51	bnj1023	$⊢ \exists j ((i \neq \emptyset \land i \in n \land χ) \to f (i) \subseteq A)$
53		3anass	$⊢ (i \neq \emptyset \land i \in n \land χ) \leftrightarrow (i \neq \emptyset \land (i \in n \land χ))$
54	53	imbi1i	$⊢ ((i \neq \emptyset \land i \in n \land χ) \to f (i) \subseteq A) \leftrightarrow ((i \neq \emptyset \land (i \in n \land χ)) \to f (i) \subseteq A)$
55	54	exbii	$⊢ \exists j ((i \neq \emptyset \land i \in n \land χ) \to f (i) \subseteq A) \leftrightarrow \exists j ((i \neq \emptyset \land (i \in n \land χ)) \to f (i) \subseteq A)$
56	52 55	mpbi	$⊢ \exists j ((i \neq \emptyset \land (i \in n \land χ)) \to f (i) \subseteq A)$
57	1	biimpi	$⊢ φ \to f (\emptyset) = pred (X, A, R)$
58	5 57	bnj771	$⊢ χ \to f (\emptyset) = pred (X, A, R)$
59		fveq2	$⊢ i = \emptyset \to f (i) = f (\emptyset)$
60		bnj213	$⊢ pred (X, A, R) \subseteq A$
61		sseq1	$⊢ f (\emptyset) = pred (X, A, R) \to (f (\emptyset) \subseteq A \leftrightarrow pred (X, A, R) \subseteq A)$
62	60 61	mpbiri	$⊢ f (\emptyset) = pred (X, A, R) \to f (\emptyset) \subseteq A$
63		sseq1	$⊢ f (i) = f (\emptyset) \to (f (i) \subseteq A \leftrightarrow f (\emptyset) \subseteq A)$
64	63	biimpar	$⊢ (f (i) = f (\emptyset) \land f (\emptyset) \subseteq A) \to f (i) \subseteq A$
65	59 62 64	syl2an	$⊢ (i = \emptyset \land f (\emptyset) = pred (X, A, R)) \to f (i) \subseteq A$
66	58 65	sylan2	$⊢ (i = \emptyset \land χ) \to f (i) \subseteq A$
67	66	adantrl	$⊢ (i = \emptyset \land (i \in n \land χ)) \to f (i) \subseteq A$
68	56 67	bnj1109	$⊢ \exists j ((i \in n \land χ) \to f (i) \subseteq A)$
69		19.9v	$⊢ \exists j ((i \in n \land χ) \to f (i) \subseteq A) \leftrightarrow ((i \in n \land χ) \to f (i) \subseteq A)$
70	68 69	mpbi	$⊢ (i \in n \land χ) \to f (i) \subseteq A$
71	70	expcom	$⊢ χ \to (i \in n \to f (i) \subseteq A)$
72		fndm	$⊢ f Fn n \to dom f = n$
73	5 72	bnj770	$⊢ χ \to dom f = n$
74		eleq2	$⊢ dom f = n \to (i \in dom f \leftrightarrow i \in n)$
75	74	imbi1d	$⊢ dom f = n \to ((i \in dom f \to f (i) \subseteq A) \leftrightarrow (i \in n \to f (i) \subseteq A))$
76	73 75	syl	$⊢ χ \to ((i \in dom f \to f (i) \subseteq A) \leftrightarrow (i \in n \to f (i) \subseteq A))$
77	71 76	mpbird	$⊢ χ \to (i \in dom f \to f (i) \subseteq A)$
78	11 77	hbralrimi	$⊢ χ \to \forall i \in dom f f (i) \subseteq A$
79	78	exlimiv	$⊢ \exists n χ \to \forall i \in dom f f (i) \subseteq A$
80	9 79	sylbi	$⊢ f \in B \to \forall i \in dom f f (i) \subseteq A$
81		ss2iun	$⊢ \forall i \in dom f f (i) \subseteq A \to ⋃_{i \in dom f} f (i) \subseteq ⋃_{i \in dom f} A$
82		bnj1143	$⊢ ⋃_{i \in dom f} A \subseteq A$
83	81 82	sstrdi	$⊢ \forall i \in dom f f (i) \subseteq A \to ⋃_{i \in dom f} f (i) \subseteq A$
84	80 83	syl	$⊢ f \in B \to ⋃_{i \in dom f} f (i) \subseteq A$
85	8 84	mprg	$⊢ ⋃_{f \in B} ⋃_{i \in dom f} f (i) \subseteq ⋃_{f \in B} A$
86	4	bnj1317	$⊢ w \in B \to \forall f w \in B$
87	86	bnj1146	$⊢ ⋃_{f \in B} A \subseteq A$
88	85 87	sstri	$⊢ ⋃_{f \in B} ⋃_{i \in dom f} f (i) \subseteq A$
89	7 88	eqsstri	$⊢ trCl (X, A, R) \subseteq A$

Metamath Proof Explorer

Theorem bnj1145

Proof