bnj594 - Mathbox for Jonathan Ben-Naim

	Mathbox for Jonathan Ben-Naim		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj594		Structured version Visualization version GIF version

Theorem bnj594 35542

Description: Technical lemma for bnj852 35551. 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
bnj594.1	⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj594.2	⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj594.3	⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
bnj594.7	⊢ 𝐷 = (ω ∖ {∅})
bnj594.9	⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj594.10	⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj594.11	⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
bnj594.15	⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
bnj594.16	⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))
bnj594.17	⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))

**Assertion**
Ref	Expression
bnj594	⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)

Distinct variable groups: 𝐴,𝑖,𝑘 𝐷,𝑘 𝑅,𝑖,𝑘 𝜒,𝑘 𝑘,𝜒′ 𝑓,𝑖,𝑘,𝑦 𝑔,𝑖,𝑘,𝑦 𝑖,𝑛,𝑘 𝑗,𝑘 Allowed substitution hints: 𝜑(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑘, 𝑛) 𝜓(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑘, 𝑛) 𝜒(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑛) 𝜃(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑘, 𝑛) 𝜏(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑘, 𝑛) 𝐴(𝑥, 𝑦, 𝑓, 𝑔, 𝑗, 𝑛) 𝐷(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑛) 𝑅(𝑥, 𝑦, 𝑓, 𝑔, 𝑗, 𝑛) 𝜑′(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑘, 𝑛) 𝜓′(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑘, 𝑛) 𝜒′(𝑥, 𝑦, 𝑓, 𝑔, 𝑖, 𝑗, 𝑛)

**Proof of Theorem bnj594**
Step	Hyp	Ref	Expression
1		bnj594.3	. . . . . . . . 9 ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
2	1	simp2bi 1164	. . . . . . . 8 ⊢ (𝜒 → 𝜑)
3		bnj594.1	. . . . . . . 8 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
4	2, 3	sylib 221	. . . . . . 7 ⊢ (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
5		bnj594.11	. . . . . . . . 9 ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
6	5	simp2bi 1164	. . . . . . . 8 ⊢ (𝜒′ → 𝜑′)
7		bnj594.9	. . . . . . . 8 ⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
8	6, 7	sylib 221	. . . . . . 7 ⊢ (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
9		eqtr3 2782	. . . . . . 7 ⊢ (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅))
10	4, 8, 9	syl2an 608	. . . . . 6 ⊢ ((𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅))
11	10	3adant1 1148	. . . . 5 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅))
12		fveq2 6885	. . . . . 6 ⊢ (𝑗 = ∅ → (𝑓‘𝑗) = (𝑓‘∅))
13		fveq2 6885	. . . . . 6 ⊢ (𝑗 = ∅ → (𝑔‘𝑗) = (𝑔‘∅))
14	12, 13	eqeq12d 2776	. . . . 5 ⊢ (𝑗 = ∅ → ((𝑓‘𝑗) = (𝑔‘𝑗) ↔ (𝑓‘∅) = (𝑔‘∅)))
15	11, 14	imbitrrid 249	. . . 4 ⊢ (𝑗 = ∅ → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
16		bnj594.15	. . . 4 ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
17	15, 16	sylibr 237	. . 3 ⊢ (𝑗 = ∅ → 𝜃)
18	17	a1d 26	. 2 ⊢ (𝑗 = ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃))
19		bnj253 35335	. . . . . 6 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′))
20		bnj252 35334	. . . . . 6 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
21		anidm 575	. . . . . . 7 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ↔ 𝑛 ∈ 𝐷)
22	21	3anbi1i 1175	. . . . . 6 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
23	19, 20, 22	3bitr3i 304	. . . . 5 ⊢ ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
24		df-bnj17 35318	. . . . . . . . . 10 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏))
25		bnj594.17	. . . . . . . . . . . 12 ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))
26	25	bnj1095 35412	. . . . . . . . . . 11 ⊢ (𝜏 → ∀𝑘𝜏)
27	26	bnj1352 35457	. . . . . . . . . 10 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏))
28	24, 27	hbxfrbi 1857	. . . . . . . . 9 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏))
29		bnj170 35329	. . . . . . . . . . . 12 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅))
30		bnj594.7	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (ω ∖ {∅})
31	30	bnj923 35399	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
32		elnn 7888	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω)
33	31, 32	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑗 ∈ ω)
34	33	anim1i 627	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
35	29, 34	sylbi 220	. . . . . . . . . . 11 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
36		nnsuc 7895	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → ∃𝑘 ∈ ω 𝑗 = suc 𝑘)
37		rexex 3092	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘)
38	35, 36, 37	3syl 19	. . . . . . . . . 10 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → ∃𝑘 𝑗 = suc 𝑘)
39	38	bnj721 35388	. . . . . . . . 9 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘 𝑗 = suc 𝑘)
40	28, 39	bnj596 35377	. . . . . . . 8 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
41		bnj667 35383	. . . . . . . . . . 11 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏))
42	41	anim1i 627	. . . . . . . . . 10 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
43		bnj258 35339	. . . . . . . . . 10 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
44	42, 43	sylibr 237	. . . . . . . . 9 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏))
45		df-bnj17 35318	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏))
46		bnj219 35364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = suc 𝑘 → 𝑘 E 𝑗)
47	46	3ad2ant3 1153	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 E 𝑗)
48	47	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗)
49		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑘 ∈ V
50	49	bnj216 35363	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = suc 𝑘 → 𝑘 ∈ 𝑗)
51		df-3an 1105	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷))
52		3anrot 1117	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗))
53		ancom 466	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)))
54	51, 52, 53	3bitr3i 304	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)))
55		eldifi 4067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ω ∖ {∅}) → 𝑛 ∈ ω)
56	55, 30	eleq2s 2878	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
57		nnord 7885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ω → Ord 𝑛)
58		ordtr1 6407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord 𝑛 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛))
59	56, 57, 58	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝐷 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛))
60	59	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)) → 𝑘 ∈ 𝑛)
61	54, 60	sylbi 220	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) → 𝑘 ∈ 𝑛)
62	50, 61	syl3an3 1183	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ 𝑛)
63		rsp 3250	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃) → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)))
64	25, 63	sylbi 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝜏 → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)))
65	62, 64	mpan9 516	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))
66	48, 65	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
67	45, 66	sylbi 220	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
68	67	anim1i 627	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
69		bnj252 35334	. . . . . . . . . . . . 13 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
70	68, 69	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
71		bnj446 35348	. . . . . . . . . . . . 13 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃))
72		bnj594.16	. . . . . . . . . . . . . 14 ⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))
73		pm3.35 815	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))) → (𝑓‘𝑘) = (𝑔‘𝑘))
74	72, 73	sylan2b 606	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓‘𝑘) = (𝑔‘𝑘))
75	71, 74	sylbi 220	. . . . . . . . . . . 12 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))
76		iuneq1 4967	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑘) = (𝑔‘𝑘) → ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
77	70, 75, 76	3syl 19	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
78		bnj658 35382	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘))
79	1	simp3bi 1165	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝜓)
80	5	simp3bi 1165	. . . . . . . . . . . . . 14 ⊢ (𝜒′ → 𝜓′)
81	79, 80	bnj240 35330	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝜓 ∧ 𝜓′))
82	78, 81	anim12i 625	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)))
83		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ 𝜓′) → 𝜓)
84	83	anim2i 629	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓))
85		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑗 = suc 𝑘)
86	85	anim1i 627	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘 ∧ 𝜓))
87		simpl1 1210	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → 𝑗 ∈ 𝑛)
88		df-3an 1105	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 = suc 𝑘))
89	88	biancomi 468	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)))
90		elnn 7888	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ ω) → 𝑘 ∈ ω)
91	50, 33, 90	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) → 𝑘 ∈ ω)
92	89, 91	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ ω)
93		bnj594.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
94	93	bnj589 35539	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑓‘suc 𝑘) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))
95	94	bnj590 35540	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 = suc 𝑘 ∧ 𝜓) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))))
96	92, 95	mpan9 516	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))
97	87, 96	mpd 16	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
98	86, 97	syldan 603	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
99	82, 84, 98	3syl 19	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
100		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ 𝜓′) → 𝜓′)
101	100	anim2i 629	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′))
102	85	anim1i 627	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘 ∧ 𝜓′))
103		simpl1 1210	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → 𝑗 ∈ 𝑛)
104		bnj594.10	. . . . . . . . . . . . . . . . 17 ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))
105	104	bnj589 35539	. . . . . . . . . . . . . . . 16 ⊢ (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑔‘suc 𝑘) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)))
106	105	bnj590 35540	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 = suc 𝑘 ∧ 𝜓′) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))))
107	92, 106	mpan9 516	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)))
108	103, 107	mpd 16	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
109	102, 108	syldan 603	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
110	82, 101, 109	3syl 19	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
111	77, 99, 110	3eqtr4d 2805	. . . . . . . . . 10 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗))
112	111	ex 418	. . . . . . . . 9 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
113	44, 112	syl 18	. . . . . . . 8 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
114	40, 113	bnj593 35376	. . . . . . 7 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
115		bnj258 35339	. . . . . . 7 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷))
116		19.9v 2016	. . . . . . 7 ⊢ (∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
117	114, 115, 116	3imtr3i 294	. . . . . 6 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
118	117	expimpd 459	. . . . 5 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗)))
119	23, 118	biimtrrid 246	. . . 4 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
120	119, 16	sylibr 237	. . 3 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)
121	120	3expib 1140	. 2 ⊢ (𝑗 ≠ ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃))
122	18, 121	pm2.61ine 3038	1 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∃wex 1811 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 [wsbc 3738 ∖ cdif 4045 ∅c0 4278 {csn 4583 ∪ ciun 4950 class class class wbr 5102 E cep 5549 Ord word 6361 suc csuc 6364 Fn wfn 6533 ‘cfv 6538 ωcom 7877 ∧ w-bnj17 35317 predc-bnj14 35319

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-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-fv 6546 df-om 7878 df-bnj17 35318

This theorem is used by: bnj580 35543

W3C validator