Theorem firest 17338

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 7385	. . . . . 6 ⊢ (𝐽 ↾t 𝐴) ∈ V
2		elfi2 9305	. . . . . 6 ⊢ ((𝐽 ↾t 𝐴) ∈ V → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦))
3	1, 2	ax-mp 5	. . . . 5 ⊢ (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦)
4		eldifi 4080	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
5	4	adantl 481	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
6	5	elin2d 4154	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
7		elfpw 9245	. . . . . . . . . . . . . 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 3929	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝐽 ↾t 𝐴)))
11		elrest 17333	. . . . . . . . . . . 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 3124	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))
15		ineq1 4162	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∩ 𝐴) = ((𝑓‘𝑧) ∩ 𝐴))
16	15	eqeq2d 2744	. . . . . . . . . 10 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑧 = (𝑦 ∩ 𝐴) ↔ 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
17	16	ac6sfi 9175	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
18	6, 14, 17	syl2anc 584	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
19		eldifsni 4741	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
20	19	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ≠ ∅)
21		iinin1 5029	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
22	20, 21	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
23		fvex 6841	. . . . . . . . . . . . 13 ⊢ (fi‘𝐽) ∈ V
24		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝐴 ∈ V)
25		ffn 6656	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝑦⟶𝐽 → 𝑓 Fn 𝑦)
26	25	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓 Fn 𝑦)
27		fniinfv 6906	. . . . . . . . . . . . . . 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 9307	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ V ∧ (𝑓:𝑦⟶𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ ran 𝑓 ∈ (fi‘𝐽))
33	29, 30, 20, 31, 32	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ ran 𝑓 ∈ (fi‘𝐽))
34	28, 33	eqeltrd 2833	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽))
35		elrestr 17334	. . . . . . . . . . . . 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 2833	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
38		intiin 5010	. . . . . . . . . . . . 13 ⊢ ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 𝑧
39		iineq2 4962	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
40	38, 39	eqtrid 2780	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
41	40	eleq1d 2818	. . . . . . . . . . 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 2821	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑦 → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
47	45, 46	syl5ibrcom 247	. . . . . 6 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
48	47	rexlimdva 3134	. . . . 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 17333	. . . . . 6 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
52	23, 50, 51	sylancr 587	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
53		elfi2 9305	. . . . . . . 8 ⊢ (𝐽 ∈ V → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
54	53	adantr 480	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
55		eldifsni 4741	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
56	55	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ≠ ∅)
57		iinin1 5029	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
58	56, 57	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
59	38	ineq1i 4165	. . . . . . . . . . . 12 ⊢ (∩ 𝑦 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)
60	58, 59	eqtr4di 2786	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
61		ovexd 7387	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝐽 ↾t 𝐴) ∈ V)
62		eldifi 4080	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
63	62	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
64		elfpw 9245	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin))
65	64	simplbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ⊆ 𝐽)
66	63, 65	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
67		elrestr 17334	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
68	67	3expa 1118	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
69	68	ralrimiva 3125	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
70	69	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
71		ssralv 3999	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝐽 → (∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)))
72	66, 70, 71	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
73	63	elin2d 4154	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
74		iinfi 9308	. . . . . . . . . . . 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 2834	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
77		eleq1 2821	. . . . . . . . . 10 ⊢ (𝑥 = (∩ 𝑦 ∩ 𝐴) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))))
78	76, 77	syl5ibrcom 247	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
79		ineq1 4162	. . . . . . . . . . 11 ⊢ (𝑧 = ∩ 𝑦 → (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
80	79	eqeq2d 2744	. . . . . . . . . 10 ⊢ (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) ↔ 𝑥 = (∩ 𝑦 ∩ 𝐴)))
81	80	imbi1d 341	. . . . . . . . 9 ⊢ (𝑧 = ∩ 𝑦 → ((𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))) ↔ (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
82	78, 81	syl5ibrcom 247	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
83	82	rexlimdva 3134	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
84	54, 83	sylbid 240	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
85	84	rexlimdv 3132	. . . . 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 2731	. 2 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴))
89		fi0 9311	. . 3 ⊢ (fi‘∅) = ∅
90		relxp 5637	. . . . . 6 ⊢ Rel (V × V)
91		restfn 17330	. . . . . . . 8 ⊢ ↾t Fn (V × V)
92	91	fndmi 6590	. . . . . . 7 ⊢ dom ↾t = (V × V)
93	92	releqi 5722	. . . . . 6 ⊢ (Rel dom ↾t ↔ Rel (V × V))
94	90, 93	mpbir 231	. . . . 5 ⊢ Rel dom ↾t
95	94	ovprc 7390	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ∅)
96	95	fveq2d 6832	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = (fi‘∅))
97		ianor 983	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) ↔ (¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V))
98		fvprc 6820	. . . . . . 7 ⊢ (¬ 𝐽 ∈ V → (fi‘𝐽) = ∅)
99	98	oveq1d 7367	. . . . . 6 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = (∅ ↾t 𝐴))
100		0rest 17335	. . . . . 6 ⊢ (∅ ↾t 𝐴) = ∅
101	99, 100	eqtrdi 2784	. . . . 5 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
102	94	ovprc2 7392	. . . . 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 2794	. 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 2113   ≠ wne 2929  ∀wral 3048  ∃wrex 3057  Vcvv 3437   ∖ cdif 3895   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  𝒫 cpw 4549  {csn 4575  ∩ cint 4897  ∩ ciin 4942   × cxp 5617  dom cdm 5619  ran crn 5620  Rel wrel 5624   Fn wfn 6481  ⟶wf 6482  ‘cfv 6486  (class class class)co 7352  Fincfn 8875  ficfi 9301   ↾_t crest 17326

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-int 4898  df-iun 4943  df-iin 4944  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7803  df-1st 7927  df-2nd 7928  df-1o 8391  df-en 8876  df-dom 8877  df-fin 8879  df-fi 9302  df-rest 17328

This theorem is referenced by:  ordtrest2  23120  xkoptsub  23570  ordtrest2NEW  33957  ptrest  37679