Theorem firest 17378

Description: The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.)

Assertion

Ref	Expression
firest	⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴)

Proof of Theorem firest

Dummy variables 𝑥 𝑓 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 7442	. . . . . 6 ⊢ (𝐽 ↾t 𝐴) ∈ V
2		elfi2 9409	. . . . . 6 ⊢ ((𝐽 ↾t 𝐴) ∈ V → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦))
3	1, 2	ax-mp 5	. . . . 5 ⊢ (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦)
4		eldifi 4127	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
5	4	adantl 483	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
6	5	elin2d 4200	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
7		elfpw 9354	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ↔ (𝑦 ⊆ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ Fin))
8	7	simplbi 499	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) → 𝑦 ⊆ (𝐽 ↾t 𝐴))
9	5, 8	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ⊆ (𝐽 ↾t 𝐴))
10	9	sseld 3982	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝐽 ↾t 𝐴)))
11		elrest 17373	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
12	11	adantr 482	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
13	10, 12	sylibd 238	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
14	13	ralrimiv 3146	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))
15		ineq1 4206	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∩ 𝐴) = ((𝑓‘𝑧) ∩ 𝐴))
16	15	eqeq2d 2744	. . . . . . . . . 10 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑧 = (𝑦 ∩ 𝐴) ↔ 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
17	16	ac6sfi 9287	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
18	6, 14, 17	syl2anc 585	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
19		eldifsni 4794	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
20	19	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ≠ ∅)
21		iinin1 5083	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
22	20, 21	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
23		fvex 6905	. . . . . . . . . . . . 13 ⊢ (fi‘𝐽) ∈ V
24		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝐴 ∈ V)
25		ffn 6718	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝑦⟶𝐽 → 𝑓 Fn 𝑦)
26	25	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓 Fn 𝑦)
27		fniinfv 6970	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑦 → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓)
28	26, 27	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓)
29		simplll 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝐽 ∈ V)
30		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓:𝑦⟶𝐽)
31	6	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ∈ Fin)
32		intrnfi 9411	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ V ∧ (𝑓:𝑦⟶𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ ran 𝑓 ∈ (fi‘𝐽))
33	29, 30, 20, 31, 32	syl13anc 1373	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ ran 𝑓 ∈ (fi‘𝐽))
34	28, 33	eqeltrd 2834	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽))
35		elrestr 17374	. . . . . . . . . . . . 13 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V ∧ ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
36	23, 24, 34, 35	mp3an2i 1467	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
37	22, 36	eqeltrd 2834	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
38		intiin 5063	. . . . . . . . . . . . 13 ⊢ ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 𝑧
39		iineq2 5018	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
40	38, 39	eqtrid 2785	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
41	40	eleq1d 2819	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → (∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)))
42	37, 41	syl5ibrcom 246	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
43	42	expimpd 455	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ((𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
44	43	exlimdv 1937	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
45	18, 44	mpd 15	. . . . . . 7 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))
46		eleq1 2822	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑦 → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
47	45, 46	syl5ibrcom 246	. . . . . 6 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
48	47	rexlimdva 3156	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
49	3, 48	biimtrid 241	. . . 4 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
50		simpr 486	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ∈ V)
51		elrest 17373	. . . . . 6 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
52	23, 50, 51	sylancr 588	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
53		elfi2 9409	. . . . . . . 8 ⊢ (𝐽 ∈ V → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
54	53	adantr 482	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
55		eldifsni 4794	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
56	55	adantl 483	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ≠ ∅)
57		iinin1 5083	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
58	56, 57	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
59	38	ineq1i 4209	. . . . . . . . . . . 12 ⊢ (∩ 𝑦 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)
60	58, 59	eqtr4di 2791	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
61		ovexd 7444	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝐽 ↾t 𝐴) ∈ V)
62		eldifi 4127	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
63	62	adantl 483	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
64		elfpw 9354	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin))
65	64	simplbi 499	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ⊆ 𝐽)
66	63, 65	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
67		elrestr 17374	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
68	67	3expa 1119	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
69	68	ralrimiva 3147	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
70	69	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
71		ssralv 4051	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝐽 → (∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)))
72	66, 70, 71	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
73	63	elin2d 4200	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
74		iinfi 9412	. . . . . . . . . . . 12 ⊢ (((𝐽 ↾t 𝐴) ∈ V ∧ (∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
75	61, 72, 56, 73, 74	syl13anc 1373	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
76	60, 75	eqeltrrd 2835	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
77		eleq1 2822	. . . . . . . . . 10 ⊢ (𝑥 = (∩ 𝑦 ∩ 𝐴) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))))
78	76, 77	syl5ibrcom 246	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
79		ineq1 4206	. . . . . . . . . . 11 ⊢ (𝑧 = ∩ 𝑦 → (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
80	79	eqeq2d 2744	. . . . . . . . . 10 ⊢ (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) ↔ 𝑥 = (∩ 𝑦 ∩ 𝐴)))
81	80	imbi1d 342	. . . . . . . . 9 ⊢ (𝑧 = ∩ 𝑦 → ((𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))) ↔ (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
82	78, 81	syl5ibrcom 246	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
83	82	rexlimdva 3156	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
84	54, 83	sylbid 239	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
85	84	rexlimdv 3154	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
86	52, 85	sylbid 239	. . . 4 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
87	49, 86	impbid 211	. . 3 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
88	87	eqrdv 2731	. 2 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴))
89		fi0 9415	. . 3 ⊢ (fi‘∅) = ∅
90		relxp 5695	. . . . . 6 ⊢ Rel (V × V)
91		restfn 17370	. . . . . . . 8 ⊢ ↾t Fn (V × V)
92	91	fndmi 6654	. . . . . . 7 ⊢ dom ↾t = (V × V)
93	92	releqi 5778	. . . . . 6 ⊢ (Rel dom ↾t ↔ Rel (V × V))
94	90, 93	mpbir 230	. . . . 5 ⊢ Rel dom ↾t
95	94	ovprc 7447	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ∅)
96	95	fveq2d 6896	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = (fi‘∅))
97		ianor 981	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) ↔ (¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V))
98		fvprc 6884	. . . . . . 7 ⊢ (¬ 𝐽 ∈ V → (fi‘𝐽) = ∅)
99	98	oveq1d 7424	. . . . . 6 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = (∅ ↾t 𝐴))
100		0rest 17375	. . . . . 6 ⊢ (∅ ↾t 𝐴) = ∅
101	99, 100	eqtrdi 2789	. . . . 5 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
102	94	ovprc2 7449	. . . . 5 ⊢ (¬ 𝐴 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
103	101, 102	jaoi 856	. . . 4 ⊢ ((¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V) → ((fi‘𝐽) ↾t 𝐴) = ∅)
104	97, 103	sylbi 216	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → ((fi‘𝐽) ↾t 𝐴) = ∅)
105	89, 96, 104	3eqtr4a 2799	. 2 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴))
106	88, 105	pm2.61i 182	1 ⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ∖ cdif 3946   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323  𝒫 cpw 4603  {csn 4629  ∩ cint 4951  ∩ ciin 4999   × cxp 5675  dom cdm 5677  ran crn 5678  Rel wrel 5682   Fn wfn 6539  ⟶wf 6540  ‘cfv 6544  (class class class)co 7409  Fincfn 8939  ficfi 9405   ↾_t crest 17366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-fin 8943  df-fi 9406  df-rest 17368

This theorem is referenced by:  ordtrest2  22708  xkoptsub  23158  ordtrest2NEW  32934  ptrest  36535