Theorem bnj1145 35007

Description: Technical lemma for bnj69 35024. 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 34940	. 2 ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
6		ss2iun 5010	. . . 4 ⊢ (∀𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴)
7		bnj1145.5	. . . . . . 7 ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
8	7, 4	bnj1083 34992	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 ↔ ∃𝑛𝜒)
9	2	bnj1095 34795	. . . . . . . . 9 ⊢ (𝜓 → ∀𝑖𝜓)
10	9, 7	bnj1096 34796	. . . . . . . 8 ⊢ (𝜒 → ∀𝑖𝜒)
11	3	bnj1098 34797	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
12	7	bnj1232 34817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑛 ∈ 𝐷)
13	12	3anim3i 1155	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))
14	11, 13	bnj1101 34798	. . . . . . . . . . . . . . . 16 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))
15		ancl 544	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
16	14, 15	bnj101 34737	. . . . . . . . . . . . . . 15 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
17		bnj1145.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))
18	17	imbi2i 336	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
19	18	exbii 1848	. . . . . . . . . . . . . . 15 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗))))
20	16, 19	mpbir 231	. . . . . . . . . . . . . 14 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝜃)
21		bnj213 34896	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
22	21	bnj226 34748	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴
23		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → 𝑖 = suc 𝑗)
24	17, 23	simplbiim 504	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 = suc 𝑗)
25		simp2 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ 𝑛)
26	12	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑛 ∈ 𝐷)
27	3	bnj923 34782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
28		elnn 7898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
29	27, 28	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑖 ∈ ω)
30	25, 26, 29	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → 𝑖 ∈ ω)
31	17, 30	bnj832 34772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ ω)
32		vex 3484	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑗 ∈ V
33	32	bnj216 34746	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖)
34		elnn 7898	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑖 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
35	33, 34	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 = suc 𝑗 ∧ 𝑖 ∈ ω) → 𝑗 ∈ ω)
36	24, 31, 35	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → 𝑗 ∈ ω)
37	17, 25	bnj832 34772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → 𝑖 ∈ 𝑛)
38	24, 37	eqeltrrd 2842	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → suc 𝑗 ∈ 𝑛)
39	2	bnj589 34923	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜓 ↔ ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
40	39	biimpi 216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜓 → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
41	40	bnj708 34770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑗 ∈ ω (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅)))
42		rsp 3247	. . . . . . . . . . . . . . . . . . . . 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 1136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
46	17, 45	bnj832 34772	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (𝑗 ∈ ω → (suc 𝑗 ∈ 𝑛 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))))
47	36, 38, 46	mp2d 49	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → (𝑓‘suc 𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑗) pred(𝑦, 𝐴, 𝑅))
48		fveqeq2 6915	. . . . . . . . . . . . . . . . 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 34824	. . . . . . . . . . . . . 14 ⊢ (𝜃 → (𝑓‘𝑖) ⊆ 𝐴)
52	20, 51	bnj1023 34794	. . . . . . . . . . . . 13 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
53		3anass 1095	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ↔ (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)))
54	53	imbi1i 349	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
55	54	exbii 1848	. . . . . . . . . . . . 13 ⊢ (∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴))
56	52, 55	mpbi 230	. . . . . . . . . . . 12 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝜒)) → (𝑓‘𝑖) ⊆ 𝐴)
57	1	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
58	7, 57	bnj771 34778	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
59		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = ∅ → (𝑓‘𝑖) = (𝑓‘∅))
60		bnj213 34896	. . . . . . . . . . . . . . . 16 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
61		sseq1 4009	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → ((𝑓‘∅) ⊆ 𝐴 ↔ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴))
62	60, 61	mpbiri 258	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) → (𝑓‘∅) ⊆ 𝐴)
63		sseq1 4009	. . . . . . . . . . . . . . . 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 34800	. . . . . . . . . . 11 ⊢ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
69		19.9v 1983	. . . . . . . . . . 11 ⊢ (∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴))
70	68, 69	mpbi 230	. . . . . . . . . 10 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜒) → (𝑓‘𝑖) ⊆ 𝐴)
71	70	expcom 413	. . . . . . . . 9 ⊢ (𝜒 → (𝑖 ∈ 𝑛 → (𝑓‘𝑖) ⊆ 𝐴))
72		fndm 6671	. . . . . . . . . . 11 ⊢ (𝑓 Fn 𝑛 → dom 𝑓 = 𝑛)
73	7, 72	bnj770 34777	. . . . . . . . . 10 ⊢ (𝜒 → dom 𝑓 = 𝑛)
74		eleq2 2830	. . . . . . . . . . 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 3144	. . . . . . 7 ⊢ (𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
79	78	exlimiv 1930	. . . . . 6 ⊢ (∃𝑛𝜒 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
80	8, 79	sylbi 217	. . . . 5 ⊢ (𝑓 ∈ 𝐵 → ∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
81		ss2iun 5010	. . . . . 6 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑖 ∈ dom 𝑓 𝐴)
82		bnj1143 34804	. . . . . 6 ⊢ ∪ 𝑖 ∈ dom 𝑓 𝐴 ⊆ 𝐴
83	81, 82	sstrdi 3996	. . . . 5 ⊢ (∀𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
84	80, 83	syl 17	. . . 4 ⊢ (𝑓 ∈ 𝐵 → ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴)
85	6, 84	mprg 3067	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴
86	4	bnj1317 34835	. . . 4 ⊢ (𝑤 ∈ 𝐵 → ∀𝑓 𝑤 ∈ 𝐵)
87	86	bnj1146 34805	. . 3 ⊢ ∪ 𝑓 ∈ 𝐵 𝐴 ⊆ 𝐴
88	85, 87	sstri 3993	. 2 ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) ⊆ 𝐴
89	5, 88	eqsstri 4030	1 ⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2714   ≠ wne 2940  ∀wral 3061  ∃wrex 3070   ∖ cdif 3948   ⊆ wss 3951  ∅c0 4333  {csn 4626  ∪ ciun 4991  dom cdm 5685  suc csuc 6386   Fn wfn 6556  ‘cfv 6561  ωcom 7887   ∧ w-bnj17 34700   predc-bnj14 34702   trClc-bnj18 34708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fn 6564  df-fv 6569  df-om 7888  df-bnj17 34701  df-bnj14 34703  df-bnj18 34709

This theorem is referenced by:  bnj1147  35008