Theorem firest 16757

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 7184	. . . . . 6 ⊢ (𝐽 ↾t 𝐴) ∈ V
2		elfi2 8904	. . . . . 6 ⊢ ((𝐽 ↾t 𝐴) ∈ V → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦))
3	1, 2	ax-mp 5	. . . . 5 ⊢ (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦)
4		eldifi 4033	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
5	4	adantl 486	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
6	5	elin2d 4105	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
7		elfpw 8852	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ↔ (𝑦 ⊆ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ Fin))
8	7	simplbi 502	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) → 𝑦 ⊆ (𝐽 ↾t 𝐴))
9	5, 8	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ⊆ (𝐽 ↾t 𝐴))
10	9	sseld 3892	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝐽 ↾t 𝐴)))
11		elrest 16752	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
12	11	adantr 485	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
13	10, 12	sylibd 242	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
14	13	ralrimiv 3113	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))
15		ineq1 4110	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∩ 𝐴) = ((𝑓‘𝑧) ∩ 𝐴))
16	15	eqeq2d 2770	. . . . . . . . . 10 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑧 = (𝑦 ∩ 𝐴) ↔ 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
17	16	ac6sfi 8788	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
18	6, 14, 17	syl2anc 588	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
19		eldifsni 4681	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
20	19	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ≠ ∅)
21		iinin1 4967	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
22	20, 21	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
23		fvex 6672	. . . . . . . . . . . . 13 ⊢ (fi‘𝐽) ∈ V
24		simpllr 776	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝐴 ∈ V)
25		ffn 6499	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝑦⟶𝐽 → 𝑓 Fn 𝑦)
26	25	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓 Fn 𝑦)
27		fniinfv 6731	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑦 → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓)
28	26, 27	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓)
29		simplll 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝐽 ∈ V)
30		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓:𝑦⟶𝐽)
31	6	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ∈ Fin)
32		intrnfi 8906	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ V ∧ (𝑓:𝑦⟶𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ ran 𝑓 ∈ (fi‘𝐽))
33	29, 30, 20, 31, 32	syl13anc 1370	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ ran 𝑓 ∈ (fi‘𝐽))
34	28, 33	eqeltrd 2853	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽))
35		elrestr 16753	. . . . . . . . . . . . 13 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V ∧ ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
36	23, 24, 34, 35	mp3an2i 1464	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
37	22, 36	eqeltrd 2853	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
38		intiin 4949	. . . . . . . . . . . . 13 ⊢ ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 𝑧
39		iineq2 4904	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
40	38, 39	syl5eq 2806	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
41	40	eleq1d 2837	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → (∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)))
42	37, 41	syl5ibrcom 250	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
43	42	expimpd 458	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ((𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
44	43	exlimdv 1935	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
45	18, 44	mpd 15	. . . . . . 7 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))
46		eleq1 2840	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑦 → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
47	45, 46	syl5ibrcom 250	. . . . . 6 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
48	47	rexlimdva 3209	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
49	3, 48	syl5bi 245	. . . 4 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
50		simpr 489	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ∈ V)
51		elrest 16752	. . . . . 6 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
52	23, 50, 51	sylancr 591	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
53		elfi2 8904	. . . . . . . 8 ⊢ (𝐽 ∈ V → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
54	53	adantr 485	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
55		eldifsni 4681	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
56	55	adantl 486	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ≠ ∅)
57		iinin1 4967	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
58	56, 57	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
59	38	ineq1i 4114	. . . . . . . . . . . 12 ⊢ (∩ 𝑦 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)
60	58, 59	eqtr4di 2812	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
61		ovexd 7186	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝐽 ↾t 𝐴) ∈ V)
62		eldifi 4033	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
63	62	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
64		elfpw 8852	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin))
65	64	simplbi 502	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ⊆ 𝐽)
66	63, 65	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
67		elrestr 16753	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
68	67	3expa 1116	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
69	68	ralrimiva 3114	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
70	69	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
71		ssralv 3959	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝐽 → (∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)))
72	66, 70, 71	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
73	63	elin2d 4105	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
74		iinfi 8907	. . . . . . . . . . . 12 ⊢ (((𝐽 ↾t 𝐴) ∈ V ∧ (∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
75	61, 72, 56, 73, 74	syl13anc 1370	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
76	60, 75	eqeltrrd 2854	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
77		eleq1 2840	. . . . . . . . . 10 ⊢ (𝑥 = (∩ 𝑦 ∩ 𝐴) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))))
78	76, 77	syl5ibrcom 250	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
79		ineq1 4110	. . . . . . . . . . 11 ⊢ (𝑧 = ∩ 𝑦 → (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
80	79	eqeq2d 2770	. . . . . . . . . 10 ⊢ (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) ↔ 𝑥 = (∩ 𝑦 ∩ 𝐴)))
81	80	imbi1d 346	. . . . . . . . 9 ⊢ (𝑧 = ∩ 𝑦 → ((𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))) ↔ (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
82	78, 81	syl5ibrcom 250	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
83	82	rexlimdva 3209	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
84	54, 83	sylbid 243	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
85	84	rexlimdv 3208	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
86	52, 85	sylbid 243	. . . 4 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
87	49, 86	impbid 215	. . 3 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
88	87	eqrdv 2757	. 2 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴))
89		fi0 8910	. . 3 ⊢ (fi‘∅) = ∅
90		relxp 5543	. . . . . 6 ⊢ Rel (V × V)
91		restfn 16749	. . . . . . . 8 ⊢ ↾t Fn (V × V)
92	91	fndmi 6438	. . . . . . 7 ⊢ dom ↾t = (V × V)
93	92	releqi 5622	. . . . . 6 ⊢ (Rel dom ↾t ↔ Rel (V × V))
94	90, 93	mpbir 234	. . . . 5 ⊢ Rel dom ↾t
95	94	ovprc 7189	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ∅)
96	95	fveq2d 6663	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = (fi‘∅))
97		ianor 980	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) ↔ (¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V))
98		fvprc 6651	. . . . . . 7 ⊢ (¬ 𝐽 ∈ V → (fi‘𝐽) = ∅)
99	98	oveq1d 7166	. . . . . 6 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = (∅ ↾t 𝐴))
100		0rest 16754	. . . . . 6 ⊢ (∅ ↾t 𝐴) = ∅
101	99, 100	eqtrdi 2810	. . . . 5 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
102	94	ovprc2 7191	. . . . 5 ⊢ (¬ 𝐴 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
103	101, 102	jaoi 855	. . . 4 ⊢ ((¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V) → ((fi‘𝐽) ↾t 𝐴) = ∅)
104	97, 103	sylbi 220	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → ((fi‘𝐽) ↾t 𝐴) = ∅)
105	89, 96, 104	3eqtr4a 2820	. 2 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴))
106	88, 105	pm2.61i 185	1 ⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 845   = wceq 1539  ∃wex 1782   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071  ∃wrex 3072  Vcvv 3410   ∖ cdif 3856   ∩ cin 3858   ⊆ wss 3859  ∅c0 4226  𝒫 cpw 4495  {csn 4523  ∩ cint 4839  ∩ ciin 4885   × cxp 5523  dom cdm 5525  ran crn 5526  Rel wrel 5530   Fn wfn 6331  ⟶wf 6332  ‘cfv 6336  (class class class)co 7151  Fincfn 8528  ficfi 8900   ↾_t crest 16745

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-1st 7694  df-2nd 7695  df-1o 8113  df-er 8300  df-en 8529  df-dom 8530  df-fin 8532  df-fi 8901  df-rest 16747

This theorem is referenced by:  ordtrest2  21897  xkoptsub  22347  ordtrest2NEW  31387  ptrest  35329