Theorem bnj1145 35005

Description: Technical lemma for bnj69 35022. 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 34938	. 2 ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
6		ss2iun 4958	. . . 4 ⊢ (∀𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴)
7		bnj1145.5	. . . . . . 7 ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
8	7, 4	bnj1083 34990	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 ↔ ∃𝑛𝜒)
9	2	bnj1095 34793	. . . . . . . . 9 ⊢ (𝜓 → ∀𝑖𝜓)
10	9, 7	bnj1096 34794	. . . . . . . 8 ⊢ (𝜒 → ∀𝑖𝜒)
11	3	bnj1098 34795	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
12	7	bnj1232 34815	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑛 ∈ 𝐷)
13	12	3anim3i 1154	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))
14	11, 13	bnj1101 34796	. . . . . . . . . . . . . . . 16 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
15		ancl 544	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
16	14, 15	bnj101 34735	. . . . . . . . . . . . . . 15 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
17		bnj1145.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
18	17	imbi2i 336	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
19	18	exbii 1849	. . . . . . . . . . . . . . 15 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
20	16, 19	mpbir 231	. . . . . . . . . . . . . 14 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃)
21		bnj213 34894	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
22	21	bnj226 34746	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
23		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → 𝑖 = suc 𝑗)
24	17, 23	simplbiim 504	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 = suc 𝑗)
25		simp2 1137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ 𝑛)
26	12	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑛 ∈ 𝐷)
27	3	bnj923 34780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
28		elnn 7807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
29	27, 28	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑖 ∈ ω)
30	25, 26, 29	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ ω)
31	17, 30	bnj832 34770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ ω)
32		vex 3440	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑗 ∈ V
33	32	bnj216 34744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖)
34		elnn 7807	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑖 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
35	33, 34	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 = suc 𝑗 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
36	24, 31, 35	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → 𝑗 ∈ ω)
37	17, 25	bnj832 34770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ 𝑛)
38	24, 37	eqeltrrd 2832	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → suc 𝑗 ∈ 𝑛)
39	2	bnj589 34921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜓 ↔ ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
40	39	biimpi 216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜓 → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
41	40	bnj708 34768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
42		rsp 3220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
43	41, 42	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
44	7, 43	sylbi 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
45	44	3ad2ant3 1135	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
46	17, 45	bnj832 34770	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
47	36, 38, 46	mp2d 49	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))
48		fveqeq2 6831	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = suc 𝑗 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
49	24, 48	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → ((𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ↔ (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
50	47, 49	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜃 → (𝑓‘𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))
51	22, 50	bnj1262 34822	. . . . . . . . . . . . . 14 ⊢ (𝜃 → (𝑓‘𝑖) ⊆ 𝐴)
52	20, 51	bnj1023 34792	. . . . . . . . . . . . 13 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
53		3anass 1094	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ↔ (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)))
54	53	imbi1i 349	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
55	54	exbii 1849	. . . . . . . . . . . . 13 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
56	52, 55	mpbi 230	. . . . . . . . . . . 12 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
57	1	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
58	7, 57	bnj771 34776	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
59		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (𝑓‘𝑖) = (𝑓‘∅))
60		bnj213 34894	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
61		sseq1 3955	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → ((𝑓‘∅) ⊆ 𝐴 ↔ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴))
62	60, 61	mpbiri 258	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → (𝑓‘∅) ⊆ 𝐴)
63		sseq1 3955	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘𝑖) = (𝑓‘∅) → ((𝑓‘𝑖) ⊆ 𝐴 ↔ (𝑓‘∅) ⊆ 𝐴))
64	63	biimpar 477	. . . . . . . . . . . . . . 15 ⊢ (((𝑓‘𝑖) = (𝑓‘∅) ∧ (𝑓‘∅) ⊆ 𝐴) → (𝑓‘𝑖) ⊆ 𝐴)
65	59, 62, 64	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = ∅ ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) → (𝑓‘𝑖) ⊆ 𝐴)
66	58, 65	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝑖 = ∅ ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
67	66	adantrl 716	. . . . . . . . . . . 12 ⊢ ((𝑖 = ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
68	56, 67	bnj1109 34798	. . . . . . . . . . 11 ⊢ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
69		19.9v 1985	. . . . . . . . . . 11 ⊢ (∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴))
70	68, 69	mpbi 230	. . . . . . . . . 10 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
71	70	expcom 413	. . . . . . . . 9 ⊢ (𝜒 → (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))
72		fndm 6584	. . . . . . . . . . 11 ⊢ (𝑓 Fn 𝑛 → dom 𝑓 = 𝑛)
73	7, 72	bnj770 34775	. . . . . . . . . 10 ⊢ (𝜒 → dom 𝑓 = 𝑛)
74		eleq2 2820	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑛 → (𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛))
75	74	imbi1d 341	. . . . . . . . . 10 ⊢ (dom 𝑓 = 𝑛 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴)))
76	73, 75	syl 17	. . . . . . . . 9 ⊢ (𝜒 → ((𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴) ↔ (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴)))
77	71, 76	mpbird 257	. . . . . . . 8 ⊢ (𝜒 → (𝑖 ∈ dom 𝑓 → (𝑓‘𝑖) ⊆ 𝐴))
78	10, 77	hbralrimi 3122	. . . . . . 7 ⊢ (𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
79	78	exlimiv 1931	. . . . . 6 ⊢ (∃𝑛𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
80	8, 79	sylbi 217	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
81		ss2iun 4958	. . . . . 6 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑖 ∈ dom 𝑓 𝐴)
82		bnj1143 34802	. . . . . 6 ⊢ ∪ 𝑖 ∈ dom 𝑓 𝐴 ⊆ 𝐴
83	81, 82	sstrdi 3942	. . . . 5 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
84	80, 83	syl 17	. . . 4 ⊢ (𝑓 ∈ 𝐵 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
85	6, 84	mprg 3053	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴
86	4	bnj1317 34833	. . . 4 ⊢ (𝑤 ∈ 𝐵 → ∀𝑓 𝑤 ∈ 𝐵)
87	86	bnj1146 34803	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 𝐴 ⊆ 𝐴
88	85, 87	sstri 3939	. 2 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴
89	5, 88	eqsstri 3976	1 ⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2111  {cab 2709   ≠ wne 2928  ∀wral 3047  ∃wrex 3056   ∖ cdif 3894   ⊆ wss 3897  ∅c0 4280  {csn 4573  ∪ ciun 4939  dom cdm 5614  suc csuc 6308   Fn wfn 6476  ‘cfv 6481  ωcom 7796   ∧ w-bnj17 34698   predc-bnj14 34700   trClc-bnj18 34706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-tr 5197  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fn 6484  df-fv 6489  df-om 7797  df-bnj17 34699  df-bnj14 34701  df-bnj18 34707

This theorem is referenced by:  bnj1147  35006