Theorem bnj1145 35623

Description: Technical lemma for bnj69 35640. 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 35556	. 2 ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
6		ss2iun 4969	. . . 4 ⊢ (∀𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴)
7		bnj1145.5	. . . . . . 7 ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
8	7, 4	bnj1083 35608	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 ↔ ∃𝑛𝜒)
9	2	bnj1095 35412	. . . . . . . . 9 ⊢ (𝜓 → ∀𝑖𝜓)
10	9, 7	bnj1096 35413	. . . . . . . 8 ⊢ (𝜒 → ∀𝑖𝜒)
11	3	bnj1098 35414	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
12	7	bnj1232 35433	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑛 ∈ 𝐷)
13	12	3anim3i 1172	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))
14	11, 13	bnj1101 35415	. . . . . . . . . . . . . . . 16 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
15		ancl 554	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
16	14, 15	bnj101 35354	. . . . . . . . . . . . . . 15 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
17		bnj1145.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
18	17	imbi2i 339	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
19	18	exbii 1880	. . . . . . . . . . . . . . 15 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
20	16, 19	mpbir 234	. . . . . . . . . . . . . 14 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃)
21		bnj213 35512	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
22	21	bnj226 35365	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
23		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → 𝑖 = suc 𝑗)
24	17, 23	simplbiim 514	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 = suc 𝑗)
25		simp2 1155	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ 𝑛)
26	12	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑛 ∈ 𝐷)
27	3	bnj923 35399	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
28		elnn 7888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
29	27, 28	sylan2 605	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑖 ∈ ω)
30	25, 26, 29	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ ω)
31	17, 30	bnj832 35389	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ ω)
32		vex 3454	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑗 ∈ V
33	32	bnj216 35363	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖)
34		elnn 7888	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑖 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
35	33, 34	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 = suc 𝑗 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
36	24, 31, 35	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → 𝑗 ∈ ω)
37	17, 25	bnj832 35389	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ 𝑛)
38	24, 37	eqeltrrd 2861	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → suc 𝑗 ∈ 𝑛)
39	2	bnj589 35539	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜓 ↔ ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
40	39	biimpi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜓 → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
41	40	bnj708 35387	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
42		rsp 3250	. . . . . . . . . . . . . . . . . . . . 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 1153	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
46	17, 45	bnj832 35389	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
47	36, 38, 46	mp2d 50	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))
48		fveqeq2 6894	. . . . . . . . . . . . . . . . 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 35440	. . . . . . . . . . . . . 14 ⊢ (𝜃 → (𝑓‘𝑖) ⊆ 𝐴)
52	20, 51	bnj1023 35411	. . . . . . . . . . . . 13 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
53		3anass 1111	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ↔ (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)))
54	53	imbi1i 352	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
55	54	exbii 1880	. . . . . . . . . . . . 13 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
56	52, 55	mpbi 233	. . . . . . . . . . . 12 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
57	1	biimpi 219	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
58	7, 57	bnj771 35395	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
59		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (𝑓‘𝑖) = (𝑓‘∅))
60		bnj213 35512	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
61		sseq1 3933	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → ((𝑓‘∅) ⊆ 𝐴 ↔ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴))
62	60, 61	mpbiri 261	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → (𝑓‘∅) ⊆ 𝐴)
63		sseq1 3933	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘𝑖) = (𝑓‘∅) → ((𝑓‘𝑖) ⊆ 𝐴 ↔ (𝑓‘∅) ⊆ 𝐴))
64	63	biimpar 483	. . . . . . . . . . . . . . 15 ⊢ (((𝑓‘𝑖) = (𝑓‘∅) ∧ (𝑓‘∅) ⊆ 𝐴) → (𝑓‘𝑖) ⊆ 𝐴)
65	59, 62, 64	syl2an 608	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = ∅ ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) → (𝑓‘𝑖) ⊆ 𝐴)
66	58, 65	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((𝑖 = ∅ ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
67	66	adantrl 729	. . . . . . . . . . . 12 ⊢ ((𝑖 = ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
68	56, 67	bnj1109 35417	. . . . . . . . . . 11 ⊢ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
69		19.9v 2016	. . . . . . . . . . 11 ⊢ (∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴))
70	68, 69	mpbi 233	. . . . . . . . . 10 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
71	70	expcom 419	. . . . . . . . 9 ⊢ (𝜒 → (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))
72		fndm 6642	. . . . . . . . . . 11 ⊢ (𝑓 Fn 𝑛 → dom 𝑓 = 𝑛)
73	7, 72	bnj770 35394	. . . . . . . . . 10 ⊢ (𝜒 → dom 𝑓 = 𝑛)
74		eleq2 2849	. . . . . . . . . . 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 3152	. . . . . . 7 ⊢ (𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
79	78	exlimiv 1962	. . . . . 6 ⊢ (∃𝑛𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
80	8, 79	sylbi 220	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
81		ss2iun 4969	. . . . . 6 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑖 ∈ dom 𝑓 𝐴)
82		bnj1143 35420	. . . . . 6 ⊢ ∪ 𝑖 ∈ dom 𝑓 𝐴 ⊆ 𝐴
83	81, 82	sstrdi 3920	. . . . 5 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
84	80, 83	syl 18	. . . 4 ⊢ (𝑓 ∈ 𝐵 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
85	6, 84	mprg 3082	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴
86	4	bnj1317 35451	. . . 4 ⊢ (𝑤 ∈ 𝐵 → ∀𝑓 𝑤 ∈ 𝐵)
87	86	bnj1146 35421	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 𝐴 ⊆ 𝐴
88	85, 87	sstri 3917	. 2 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴
89	5, 88	eqsstri 3954	1 ⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086   ⊆ wss 3895   ∖ cdif 4045  ∅c0 4278  {csn 4583  ∪ ciun 4950  dom cdm 5650  suc csuc 6364   Fn wfn 6533  ‘cfv 6538  ωcom 7877   ∧ w-bnj17 35317   predc-bnj14 35319   trClc-bnj18 35325

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fn 6541  df-fv 6546  df-om 7878  df-bnj17 35318  df-bnj14 35320  df-bnj18 35326

This theorem is used by:  bnj1147  35624