Theorem bnj1145 35390

Description: Technical lemma for bnj69 35407. 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.)

Hypotheses

Ref	Expression
bnj1145.1	⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
bnj1145.2	⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj1145.3	⊢ 𝐷 = (ω ∖ {∅})
bnj1145.4	⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
bnj1145.5	⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
bnj1145.6	⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))

Assertion

Ref	Expression
bnj1145	⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴

Distinct variable groups:   𝐴,𝑓,𝑖,𝑗,𝑛,𝑦   𝐷,𝑖,𝑗   𝑅,𝑓,𝑖,𝑗,𝑛,𝑦   𝑓,𝑋,𝑖,𝑛,𝑦   𝜒,𝑗   𝜑,𝑖

Allowed substitution hints:   𝜑(𝑦, 𝑓, 𝑗, 𝑛)   𝜓(𝑦, 𝑓, 𝑖, 𝑗, 𝑛)   𝜒(𝑦, 𝑓, 𝑖, 𝑛)   𝜃(𝑦, 𝑓, 𝑖, 𝑗, 𝑛)   𝐵(𝑦, 𝑓, 𝑖, 𝑗, 𝑛)   𝐷(𝑦, 𝑓, 𝑛)   𝑋(𝑗)

Proof of Theorem bnj1145

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bnj1145.1	. . 3 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
2		bnj1145.2	. . 3 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
3		bnj1145.3	. . 3 ⊢ 𝐷 = (ω ∖ {∅})
4		bnj1145.4	. . 3 ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
5	1, 2, 3, 4	bnj882 35323	. 2 ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
6		ss2iun 4974	. . . 4 ⊢ (∀𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴)
7		bnj1145.5	. . . . . . 7 ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
8	7, 4	bnj1083 35375	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 ↔ ∃𝑛𝜒)
9	2	bnj1095 35179	. . . . . . . . 9 ⊢ (𝜓 → ∀𝑖𝜓)
10	9, 7	bnj1096 35180	. . . . . . . 8 ⊢ (𝜒 → ∀𝑖𝜒)
11	3	bnj1098 35181	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
12	7	bnj1232 35200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑛 ∈ 𝐷)
13	12	3anim3i 1171	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))
14	11, 13	bnj1101 35182	. . . . . . . . . . . . . . . 16 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
15		ancl 553	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
16	14, 15	bnj101 35121	. . . . . . . . . . . . . . 15 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
17		bnj1145.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
18	17	imbi2i 339	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
19	18	exbii 1877	. . . . . . . . . . . . . . 15 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
20	16, 19	mpbir 234	. . . . . . . . . . . . . 14 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃)
21		bnj213 35279	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
22	21	bnj226 35132	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
23		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → 𝑖 = suc 𝑗)
24	17, 23	simplbiim 513	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 = suc 𝑗)
25		simp2 1154	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ 𝑛)
26	12	3ad2ant3 1152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑛 ∈ 𝐷)
27	3	bnj923 35166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
28		elnn 7871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
29	27, 28	sylan2 604	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑖 ∈ ω)
30	25, 26, 29	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ ω)
31	17, 30	bnj832 35156	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ ω)
32		vex 3458	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑗 ∈ V
33	32	bnj216 35130	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖)
34		elnn 7871	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑖 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
35	33, 34	sylan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 = suc 𝑗 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
36	24, 31, 35	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → 𝑗 ∈ ω)
37	17, 25	bnj832 35156	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ 𝑛)
38	24, 37	eqeltrrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → suc 𝑗 ∈ 𝑛)
39	2	bnj589 35306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜓 ↔ ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
40	39	biimpi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜓 → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
41	40	bnj708 35154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
42		rsp 3252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
43	41, 42	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
44	7, 43	sylbi 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
45	44	3ad2ant3 1152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
46	17, 45	bnj832 35156	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
47	36, 38, 46	mp2d 50	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))
48		fveqeq2 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = suc 𝑗 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
49	24, 48	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
50	47, 49	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜃 → (𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))
51	22, 50	bnj1262 35207	. . . . . . . . . . . . . 14 ⊢ (𝜃 → (𝑓‘𝑖) ⊆ 𝐴)
52	20, 51	bnj1023 35178	. . . . . . . . . . . . 13 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
53		3anass 1110	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ↔ (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)))
54	53	imbi1i 352	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
55	54	exbii 1877	. . . . . . . . . . . . 13 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
56	52, 55	mpbi 233	. . . . . . . . . . . 12 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
57	1	biimpi 219	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
58	7, 57	bnj771 35162	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
59		fveq2 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (𝑓‘𝑖) = (𝑓‘∅))
60		bnj213 35279	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
61		sseq1 3961	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → ((𝑓‘∅) ⊆ 𝐴 ↔ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴))
62	60, 61	mpbiri 261	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → (𝑓‘∅) ⊆ 𝐴)
63		sseq1 3961	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘𝑖) = (𝑓‘∅) → ((𝑓‘𝑖) ⊆ 𝐴 ↔ (𝑓‘∅) ⊆ 𝐴))
64	63	biimpar 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑓‘𝑖) = (𝑓‘∅) ∧ (𝑓‘∅) ⊆ 𝐴) → (𝑓‘𝑖) ⊆ 𝐴)
65	59, 62, 64	syl2an 607	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = ∅ ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) → (𝑓‘𝑖) ⊆ 𝐴)
66	58, 65	sylan2 604	. . . . . . . . . . . . 13 ⊢ ((𝑖 = ∅ ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
67	66	adantrl 728	. . . . . . . . . . . 12 ⊢ ((𝑖 = ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
68	56, 67	bnj1109 35184	. . . . . . . . . . 11 ⊢ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
69		19.9v 2013	. . . . . . . . . . 11 ⊢ (∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴))
70	68, 69	mpbi 233	. . . . . . . . . 10 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
71	70	expcom 418	. . . . . . . . 9 ⊢ (𝜒 → (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))
72		fndm 6638	. . . . . . . . . . 11 ⊢ (𝑓 Fn 𝑛 → dom 𝑓 = 𝑛)
73	7, 72	bnj770 35161	. . . . . . . . . 10 ⊢ (𝜒 → dom 𝑓 = 𝑛)
74		eleq2 2851	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑛 → (𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛))
75	74	imbi1d 344	. . . . . . . . . 10 ⊢ (dom 𝑓 = 𝑛 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴)))
76	73, 75	syl 18	. . . . . . . . 9 ⊢ (𝜒 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴)))
77	71, 76	mpbird 260	. . . . . . . 8 ⊢ (𝜒 → (𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴))
78	10, 77	hbralrimi 3154	. . . . . . 7 ⊢ (𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
79	78	exlimiv 1959	. . . . . 6 ⊢ (∃𝑛𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
80	8, 79	sylbi 220	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
81		ss2iun 4974	. . . . . 6 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑖 ∈ dom 𝑓 𝐴)
82		bnj1143 35187	. . . . . 6 ⊢ ∪ 𝑖 ∈ dom 𝑓 𝐴 ⊆ 𝐴
83	81, 82	sstrdi 3948	. . . . 5 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
84	80, 83	syl 18	. . . 4 ⊢ (𝑓 ∈ 𝐵 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
85	6, 84	mprg 3084	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴
86	4	bnj1317 35218	. . . 4 ⊢ (𝑤 ∈ 𝐵 → ∀𝑓 𝑤 ∈ 𝐵)
87	86	bnj1146 35188	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 𝐴 ⊆ 𝐴
88	85, 87	sstri 3945	. 2 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴
89	5, 88	eqsstri 3982	1 ⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102   = wceq 1569  ∃wex 1808   ∈ wcel 2142  {cab 2740   ≠ wne 2957  ∀wral 3078  ∃wrex 3088   ∖ cdif 3901   ⊆ wss 3904  ∅c0 4285  {csn 4588  ∪ ciun 4955  dom cdm 5660  suc csuc 6362   Fn wfn 6531  ‘cfv 6536  ωcom 7860   ∧ w-bnj17 35084   predc-bnj14 35086   trClc-bnj18 35092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-tr 5218  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fn 6539  df-fv 6544  df-om 7861  df-bnj17 35085  df-bnj14 35087  df-bnj18 35093

This theorem is used by:  bnj1147  35391