Theorem bnj1145 32873

Description: Technical lemma for bnj69 32890. 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 32806	. 2 ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
6		ss2iun 4939	. . . 4 ⊢ (∀𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴)
7		bnj1145.5	. . . . . . 7 ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
8	7, 4	bnj1083 32858	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 ↔ ∃𝑛𝜒)
9	2	bnj1095 32661	. . . . . . . . 9 ⊢ (𝜓 → ∀𝑖𝜓)
10	9, 7	bnj1096 32662	. . . . . . . 8 ⊢ (𝜒 → ∀𝑖𝜒)
11	3	bnj1098 32663	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
12	7	bnj1232 32683	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑛 ∈ 𝐷)
13	12	3anim3i 1152	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))
14	11, 13	bnj1101 32664	. . . . . . . . . . . . . . . 16 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
15		ancl 544	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
16	14, 15	bnj101 32602	. . . . . . . . . . . . . . 15 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
17		bnj1145.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
18	17	imbi2i 335	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
19	18	exbii 1851	. . . . . . . . . . . . . . 15 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
20	16, 19	mpbir 230	. . . . . . . . . . . . . 14 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃)
21		bnj213 32762	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
22	21	bnj226 32613	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
23		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → 𝑖 = suc 𝑗)
24	17, 23	simplbiim 504	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 = suc 𝑗)
25		simp2 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ 𝑛)
26	12	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑛 ∈ 𝐷)
27	3	bnj923 32648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
28		elnn 7698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
29	27, 28	sylan2 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑖 ∈ ω)
30	25, 26, 29	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ ω)
31	17, 30	bnj832 32638	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ ω)
32		vex 3426	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑗 ∈ V
33	32	bnj216 32611	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖)
34		elnn 7698	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑖 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
35	33, 34	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 = suc 𝑗 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
36	24, 31, 35	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → 𝑗 ∈ ω)
37	17, 25	bnj832 32638	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ 𝑛)
38	24, 37	eqeltrrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → suc 𝑗 ∈ 𝑛)
39	2	bnj589 32789	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜓 ↔ ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
40	39	biimpi 215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜓 → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
41	40	bnj708 32636	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
42		rsp 3129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
43	41, 42	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
44	7, 43	sylbi 216	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
45	44	3ad2ant3 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
46	17, 45	bnj832 32638	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
47	36, 38, 46	mp2d 49	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))
48		fveqeq2 6765	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = suc 𝑗 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
49	24, 48	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
50	47, 49	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (𝜃 → (𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))
51	22, 50	bnj1262 32690	. . . . . . . . . . . . . 14 ⊢ (𝜃 → (𝑓‘𝑖) ⊆ 𝐴)
52	20, 51	bnj1023 32660	. . . . . . . . . . . . 13 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
53		3anass 1093	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ↔ (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)))
54	53	imbi1i 349	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
55	54	exbii 1851	. . . . . . . . . . . . 13 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
56	52, 55	mpbi 229	. . . . . . . . . . . 12 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
57	1	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
58	7, 57	bnj771 32644	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
59		fveq2 6756	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (𝑓‘𝑖) = (𝑓‘∅))
60		bnj213 32762	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
61		sseq1 3942	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → ((𝑓‘∅) ⊆ 𝐴 ↔ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴))
62	60, 61	mpbiri 257	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → (𝑓‘∅) ⊆ 𝐴)
63		sseq1 3942	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘𝑖) = (𝑓‘∅) → ((𝑓‘𝑖) ⊆ 𝐴 ↔ (𝑓‘∅) ⊆ 𝐴))
64	63	biimpar 477	. . . . . . . . . . . . . . 15 ⊢ (((𝑓‘𝑖) = (𝑓‘∅) ∧ (𝑓‘∅) ⊆ 𝐴) → (𝑓‘𝑖) ⊆ 𝐴)
65	59, 62, 64	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = ∅ ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) → (𝑓‘𝑖) ⊆ 𝐴)
66	58, 65	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((𝑖 = ∅ ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
67	66	adantrl 712	. . . . . . . . . . . 12 ⊢ ((𝑖 = ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
68	56, 67	bnj1109 32666	. . . . . . . . . . 11 ⊢ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
69		19.9v 1988	. . . . . . . . . . 11 ⊢ (∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴))
70	68, 69	mpbi 229	. . . . . . . . . 10 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
71	70	expcom 413	. . . . . . . . 9 ⊢ (𝜒 → (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))
72		fndm 6520	. . . . . . . . . . 11 ⊢ (𝑓 Fn 𝑛 → dom 𝑓 = 𝑛)
73	7, 72	bnj770 32643	. . . . . . . . . 10 ⊢ (𝜒 → dom 𝑓 = 𝑛)
74		eleq2 2827	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑛 → (𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛))
75	74	imbi1d 341	. . . . . . . . . 10 ⊢ (dom 𝑓 = 𝑛 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴)))
76	73, 75	syl 17	. . . . . . . . 9 ⊢ (𝜒 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴)))
77	71, 76	mpbird 256	. . . . . . . 8 ⊢ (𝜒 → (𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴))
78	10, 77	hbralrimi 3105	. . . . . . 7 ⊢ (𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
79	78	exlimiv 1934	. . . . . 6 ⊢ (∃𝑛𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
80	8, 79	sylbi 216	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
81		ss2iun 4939	. . . . . 6 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑖 ∈ dom 𝑓 𝐴)
82		bnj1143 32670	. . . . . 6 ⊢ ∪ 𝑖 ∈ dom 𝑓 𝐴 ⊆ 𝐴
83	81, 82	sstrdi 3929	. . . . 5 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
84	80, 83	syl 17	. . . 4 ⊢ (𝑓 ∈ 𝐵 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
85	6, 84	mprg 3077	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴
86	4	bnj1317 32701	. . . 4 ⊢ (𝑤 ∈ 𝐵 → ∀𝑓 𝑤 ∈ 𝐵)
87	86	bnj1146 32671	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 𝐴 ⊆ 𝐴
88	85, 87	sstri 3926	. 2 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴
89	5, 88	eqsstri 3951	1 ⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715   ≠ wne 2942  ∀wral 3063  ∃wrex 3064   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4253  {csn 4558  ∪ ciun 4921  dom cdm 5580  suc csuc 6253   Fn wfn 6413  ‘cfv 6418  ωcom 7687   ∧ w-bnj17 32565   predc-bnj14 32567   trClc-bnj18 32573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-tr 5188  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fn 6421  df-fv 6426  df-om 7688  df-bnj17 32566  df-bnj14 32568  df-bnj18 32574

This theorem is referenced by:  bnj1147  32874