Theorem bnj594 34926

Description: Technical lemma for bnj852 34935. 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 1147	. . . . . . . 8 ⊢ (𝜒 → 𝜑)
3		bnj594.1	. . . . . . . 8 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
4	2, 3	sylib 218	. . . . . . 7 ⊢ (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
5		bnj594.11	. . . . . . . . 9 ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
6	5	simp2bi 1147	. . . . . . . 8 ⊢ (𝜒′ → 𝜑′)
7		bnj594.9	. . . . . . . 8 ⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
8	6, 7	sylib 218	. . . . . . 7 ⊢ (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
9		eqtr3 2763	. . . . . . 7 ⊢ (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅))
10	4, 8, 9	syl2an 596	. . . . . 6 ⊢ ((𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅))
11	10	3adant1 1131	. . . . 5 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅))
12		fveq2 6906	. . . . . 6 ⊢ (𝑗 = ∅ → (𝑓‘𝑗) = (𝑓‘∅))
13		fveq2 6906	. . . . . 6 ⊢ (𝑗 = ∅ → (𝑔‘𝑗) = (𝑔‘∅))
14	12, 13	eqeq12d 2753	. . . . 5 ⊢ (𝑗 = ∅ → ((𝑓‘𝑗) = (𝑔‘𝑗) ↔ (𝑓‘∅) = (𝑔‘∅)))
15	11, 14	imbitrrid 246	. . . 4 ⊢ (𝑗 = ∅ → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
16		bnj594.15	. . . 4 ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
17	15, 16	sylibr 234	. . 3 ⊢ (𝑗 = ∅ → 𝜃)
18	17	a1d 25	. 2 ⊢ (𝑗 = ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃))
19		bnj253 34718	. . . . . 6 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′))
20		bnj252 34717	. . . . . 6 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
21		anidm 564	. . . . . . 7 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ↔ 𝑛 ∈ 𝐷)
22	21	3anbi1i 1158	. . . . . 6 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
23	19, 20, 22	3bitr3i 301	. . . . 5 ⊢ ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
24		df-bnj17 34701	. . . . . . . . . 10 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏))
25		bnj594.17	. . . . . . . . . . . 12 ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))
26	25	bnj1095 34795	. . . . . . . . . . 11 ⊢ (𝜏 → ∀𝑘𝜏)
27	26	bnj1352 34841	. . . . . . . . . 10 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏))
28	24, 27	hbxfrbi 1825	. . . . . . . . 9 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏))
29		bnj170 34712	. . . . . . . . . . . 12 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅))
30		bnj594.7	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (ω ∖ {∅})
31	30	bnj923 34782	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
32		elnn 7898	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω)
33	31, 32	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑗 ∈ ω)
34	33	anim1i 615	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
35	29, 34	sylbi 217	. . . . . . . . . . 11 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
36		nnsuc 7905	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → ∃𝑘 ∈ ω 𝑗 = suc 𝑘)
37		rexex 3076	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘)
38	35, 36, 37	3syl 18	. . . . . . . . . 10 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → ∃𝑘 𝑗 = suc 𝑘)
39	38	bnj721 34771	. . . . . . . . 9 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘 𝑗 = suc 𝑘)
40	28, 39	bnj596 34760	. . . . . . . 8 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
41		bnj667 34766	. . . . . . . . . . 11 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏))
42	41	anim1i 615	. . . . . . . . . 10 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
43		bnj258 34722	. . . . . . . . . 10 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
44	42, 43	sylibr 234	. . . . . . . . 9 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏))
45		df-bnj17 34701	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏))
46		bnj219 34747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = suc 𝑘 → 𝑘 E 𝑗)
47	46	3ad2ant3 1136	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 E 𝑗)
48	47	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗)
49		vex 3484	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑘 ∈ V
50	49	bnj216 34746	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = suc 𝑘 → 𝑘 ∈ 𝑗)
51		df-3an 1089	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷))
52		3anrot 1100	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗))
53		ancom 460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)))
54	51, 52, 53	3bitr3i 301	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)))
55		eldifi 4131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ω ∖ {∅}) → 𝑛 ∈ ω)
56	55, 30	eleq2s 2859	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
57		nnord 7895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ω → Ord 𝑛)
58		ordtr1 6427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord 𝑛 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛))
59	56, 57, 58	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝐷 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛))
60	59	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)) → 𝑘 ∈ 𝑛)
61	54, 60	sylbi 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) → 𝑘 ∈ 𝑛)
62	50, 61	syl3an3 1166	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ 𝑛)
63		rsp 3247	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃) → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)))
64	25, 63	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝜏 → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)))
65	62, 64	mpan9 506	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))
66	48, 65	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
67	45, 66	sylbi 217	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
68	67	anim1i 615	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
69		bnj252 34717	. . . . . . . . . . . . 13 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
70	68, 69	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
71		bnj446 34731	. . . . . . . . . . . . 13 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃))
72		bnj594.16	. . . . . . . . . . . . . 14 ⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))
73		pm3.35 803	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))) → (𝑓‘𝑘) = (𝑔‘𝑘))
74	72, 73	sylan2b 594	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓‘𝑘) = (𝑔‘𝑘))
75	71, 74	sylbi 217	. . . . . . . . . . . 12 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))
76		iuneq1 5008	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑘) = (𝑔‘𝑘) → ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
77	70, 75, 76	3syl 18	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
78		bnj658 34765	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘))
79	1	simp3bi 1148	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝜓)
80	5	simp3bi 1148	. . . . . . . . . . . . . 14 ⊢ (𝜒′ → 𝜓′)
81	79, 80	bnj240 34713	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝜓 ∧ 𝜓′))
82	78, 81	anim12i 613	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)))
83		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ 𝜓′) → 𝜓)
84	83	anim2i 617	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓))
85		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑗 = suc 𝑘)
86	85	anim1i 615	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘 ∧ 𝜓))
87		simpl1 1192	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → 𝑗 ∈ 𝑛)
88		df-3an 1089	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 = suc 𝑘))
89	88	biancomi 462	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)))
90		elnn 7898	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ ω) → 𝑘 ∈ ω)
91	50, 33, 90	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) → 𝑘 ∈ ω)
92	89, 91	sylbi 217	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ ω)
93		bnj594.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
94	93	bnj589 34923	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑓‘suc 𝑘) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))
95	94	bnj590 34924	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 = suc 𝑘 ∧ 𝜓) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))))
96	92, 95	mpan9 506	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))
97	87, 96	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
98	86, 97	syldan 591	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
99	82, 84, 98	3syl 18	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
100		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ 𝜓′) → 𝜓′)
101	100	anim2i 617	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′))
102	85	anim1i 615	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘 ∧ 𝜓′))
103		simpl1 1192	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → 𝑗 ∈ 𝑛)
104		bnj594.10	. . . . . . . . . . . . . . . . 17 ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))
105	104	bnj589 34923	. . . . . . . . . . . . . . . 16 ⊢ (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑔‘suc 𝑘) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)))
106	105	bnj590 34924	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 = suc 𝑘 ∧ 𝜓′) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))))
107	92, 106	mpan9 506	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)))
108	103, 107	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
109	102, 108	syldan 591	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
110	82, 101, 109	3syl 18	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
111	77, 99, 110	3eqtr4d 2787	. . . . . . . . . 10 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗))
112	111	ex 412	. . . . . . . . 9 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
113	44, 112	syl 17	. . . . . . . 8 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
114	40, 113	bnj593 34759	. . . . . . 7 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
115		bnj258 34722	. . . . . . 7 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷))
116		19.9v 1983	. . . . . . 7 ⊢ (∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
117	114, 115, 116	3imtr3i 291	. . . . . 6 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
118	117	expimpd 453	. . . . 5 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗)))
119	23, 118	biimtrrid 243	. . . 4 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
120	119, 16	sylibr 234	. . 3 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)
121	120	3expib 1123	. 2 ⊢ (𝑗 ≠ ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃))
122	18, 121	pm2.61ine 3025	1 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  [wsbc 3788   ∖ cdif 3948  ∅c0 4333  {csn 4626  ∪ ciun 4991   class class class wbr 5143   E cep 5583  Ord word 6383  suc csuc 6386   Fn wfn 6556  ‘cfv 6561  ωcom 7887   ∧ w-bnj17 34700   predc-bnj14 34702

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-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-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-fv 6569  df-om 7888  df-bnj17 34701

This theorem is referenced by:  bnj580  34927