Theorem firest 17333

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 7379	. . . . . 6 ⊢ (𝐽 ↾t 𝐴) ∈ V
2		elfi2 9298	. . . . . 6 ⊢ ((𝐽 ↾t 𝐴) ∈ V → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦))
3	1, 2	ax-mp 5	. . . . 5 ⊢ (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦)
4		eldifi 4081	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
5	4	adantl 481	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
6	5	elin2d 4155	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
7		elfpw 9238	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ↔ (𝑦 ⊆ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ Fin))
8	7	simplbi 497	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) → 𝑦 ⊆ (𝐽 ↾t 𝐴))
9	5, 8	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ⊆ (𝐽 ↾t 𝐴))
10	9	sseld 3933	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝐽 ↾t 𝐴)))
11		elrest 17328	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
12	11	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
13	10, 12	sylibd 239	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
14	13	ralrimiv 3123	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))
15		ineq1 4163	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∩ 𝐴) = ((𝑓‘𝑧) ∩ 𝐴))
16	15	eqeq2d 2742	. . . . . . . . . 10 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑧 = (𝑦 ∩ 𝐴) ↔ 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
17	16	ac6sfi 9168	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
18	6, 14, 17	syl2anc 584	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
19		eldifsni 4742	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
20	19	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ≠ ∅)
21		iinin1 5027	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
22	20, 21	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
23		fvex 6835	. . . . . . . . . . . . 13 ⊢ (fi‘𝐽) ∈ V
24		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝐴 ∈ V)
25		ffn 6651	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝑦⟶𝐽 → 𝑓 Fn 𝑦)
26	25	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓 Fn 𝑦)
27		fniinfv 6900	. . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓:𝑦⟶𝐽)
31	6	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ∈ Fin)
32		intrnfi 9300	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ V ∧ (𝑓:𝑦⟶𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ ran 𝑓 ∈ (fi‘𝐽))
33	29, 30, 20, 31, 32	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ ran 𝑓 ∈ (fi‘𝐽))
34	28, 33	eqeltrd 2831	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽))
35		elrestr 17329	. . . . . . . . . . . . 13 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V ∧ ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
36	23, 24, 34, 35	mp3an2i 1468	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
37	22, 36	eqeltrd 2831	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
38		intiin 5008	. . . . . . . . . . . . 13 ⊢ ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 𝑧
39		iineq2 4962	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
40	38, 39	eqtrid 2778	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
41	40	eleq1d 2816	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → (∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)))
42	37, 41	syl5ibrcom 247	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
43	42	expimpd 453	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ((𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
44	43	exlimdv 1934	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
45	18, 44	mpd 15	. . . . . . 7 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))
46		eleq1 2819	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑦 → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
47	45, 46	syl5ibrcom 247	. . . . . 6 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
48	47	rexlimdva 3133	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
49	3, 48	biimtrid 242	. . . 4 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
50		simpr 484	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ∈ V)
51		elrest 17328	. . . . . 6 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
52	23, 50, 51	sylancr 587	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
53		elfi2 9298	. . . . . . . 8 ⊢ (𝐽 ∈ V → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
54	53	adantr 480	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
55		eldifsni 4742	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
56	55	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ≠ ∅)
57		iinin1 5027	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
58	56, 57	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
59	38	ineq1i 4166	. . . . . . . . . . . 12 ⊢ (∩ 𝑦 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)
60	58, 59	eqtr4di 2784	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
61		ovexd 7381	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝐽 ↾t 𝐴) ∈ V)
62		eldifi 4081	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
63	62	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
64		elfpw 9238	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin))
65	64	simplbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ⊆ 𝐽)
66	63, 65	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
67		elrestr 17329	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
68	67	3expa 1118	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
69	68	ralrimiva 3124	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
70	69	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
71		ssralv 4003	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝐽 → (∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)))
72	66, 70, 71	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
73	63	elin2d 4155	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
74		iinfi 9301	. . . . . . . . . . . 12 ⊢ (((𝐽 ↾t 𝐴) ∈ V ∧ (∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
75	61, 72, 56, 73, 74	syl13anc 1374	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
76	60, 75	eqeltrrd 2832	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
77		eleq1 2819	. . . . . . . . . 10 ⊢ (𝑥 = (∩ 𝑦 ∩ 𝐴) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))))
78	76, 77	syl5ibrcom 247	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
79		ineq1 4163	. . . . . . . . . . 11 ⊢ (𝑧 = ∩ 𝑦 → (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
80	79	eqeq2d 2742	. . . . . . . . . 10 ⊢ (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) ↔ 𝑥 = (∩ 𝑦 ∩ 𝐴)))
81	80	imbi1d 341	. . . . . . . . 9 ⊢ (𝑧 = ∩ 𝑦 → ((𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))) ↔ (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
82	78, 81	syl5ibrcom 247	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
83	82	rexlimdva 3133	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
84	54, 83	sylbid 240	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
85	84	rexlimdv 3131	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
86	52, 85	sylbid 240	. . . 4 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
87	49, 86	impbid 212	. . 3 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
88	87	eqrdv 2729	. 2 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴))
89		fi0 9304	. . 3 ⊢ (fi‘∅) = ∅
90		relxp 5634	. . . . . 6 ⊢ Rel (V × V)
91		restfn 17325	. . . . . . . 8 ⊢ ↾t Fn (V × V)
92	91	fndmi 6585	. . . . . . 7 ⊢ dom ↾t = (V × V)
93	92	releqi 5718	. . . . . 6 ⊢ (Rel dom ↾t ↔ Rel (V × V))
94	90, 93	mpbir 231	. . . . 5 ⊢ Rel dom ↾t
95	94	ovprc 7384	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ∅)
96	95	fveq2d 6826	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = (fi‘∅))
97		ianor 983	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) ↔ (¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V))
98		fvprc 6814	. . . . . . 7 ⊢ (¬ 𝐽 ∈ V → (fi‘𝐽) = ∅)
99	98	oveq1d 7361	. . . . . 6 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = (∅ ↾t 𝐴))
100		0rest 17330	. . . . . 6 ⊢ (∅ ↾t 𝐴) = ∅
101	99, 100	eqtrdi 2782	. . . . 5 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
102	94	ovprc2 7386	. . . . 5 ⊢ (¬ 𝐴 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
103	101, 102	jaoi 857	. . . 4 ⊢ ((¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V) → ((fi‘𝐽) ↾t 𝐴) = ∅)
104	97, 103	sylbi 217	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → ((fi‘𝐽) ↾t 𝐴) = ∅)
105	89, 96, 104	3eqtr4a 2792	. 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 206   ∧ wa 395   ∨ wo 847   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ∖ cdif 3899   ∩ cin 3901   ⊆ wss 3902  ∅c0 4283  𝒫 cpw 4550  {csn 4576  ∩ cint 4897  ∩ ciin 4942   × cxp 5614  dom cdm 5616  ran crn 5617  Rel wrel 5621   Fn wfn 6476  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346  Fincfn 8869  ficfi 9294   ↾_t crest 17321

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-rep 5217  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  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-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-int 4898  df-iun 4943  df-iin 4944  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-1st 7921  df-2nd 7922  df-1o 8385  df-en 8870  df-dom 8871  df-fin 8873  df-fi 9295  df-rest 17323

This theorem is referenced by:  ordtrest2  23117  xkoptsub  23567  ordtrest2NEW  33931  ptrest  37658