Theorem firest 17608

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 7453	. . . . . 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 4067	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
5	4	adantl 487	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin))
6	5	elin2d 4102	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
7		elfpw 9346	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ↔ (𝑦 ⊆ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ Fin))
8	7	simplbi 502	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) → 𝑦 ⊆ (𝐽 ↾t 𝐴))
9	5, 8	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → 𝑦 ⊆ (𝐽 ↾t 𝐴))
10	9	sseld 3907	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝐽 ↾t 𝐴)))
11		elrest 17603	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
12	11	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
13	10, 12	sylibd 242	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑧 ∈ 𝑦 → ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)))
14	13	ralrimiv 3153	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))
15		ineq1 4110	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∩ 𝐴) = ((𝑓‘𝑧) ∩ 𝐴))
16	15	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑦 = (𝑓‘𝑧) → (𝑧 = (𝑦 ∩ 𝐴) ↔ 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
17	16	ac6sfi 9278	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
18	6, 14, 17	syl2anc 596	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)))
19		eldifsni 4749	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
20	19	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ≠ ∅)
21		iinin1 5038	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
22	20, 21	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴))
23		fvex 6898	. . . . . . . . . . . . 13 ⊢ (fi‘𝐽) ∈ V
24		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝐴 ∈ V)
25		ffn 6709	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝑦⟶𝐽 → 𝑓 Fn 𝑦)
26	25	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓 Fn 𝑦)
27		fniinfv 6963	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑦 → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓)
28	26, 27	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓)
29		simplll 787	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝐽 ∈ V)
30		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑓:𝑦⟶𝐽)
31	6	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → 𝑦 ∈ Fin)
32		intrnfi 9411	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ V ∧ (𝑓:𝑦⟶𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ ran 𝑓 ∈ (fi‘𝐽))
33	29, 30, 20, 31, 32	syl13anc 1399	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ ran 𝑓 ∈ (fi‘𝐽))
34	28, 33	eqeltrd 2860	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽))
35		elrestr 17604	. . . . . . . . . . . . 13 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V ∧ ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
36	23, 24, 34, 35	mp3an2i 1495	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
37	22, 36	eqeltrd 2860	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))
38		intiin 5017	. . . . . . . . . . . . 13 ⊢ ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 𝑧
39		iineq2 4971	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
40	38, 39	eqtrid 2807	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴))
41	40	eleq1d 2845	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → (∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)))
42	37, 41	syl5ibrcom 250	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) ∧ 𝑓:𝑦⟶𝐽) → (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
43	42	expimpd 459	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ((𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
44	43	exlimdv 1965	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
45	18, 44	mpd 16	. . . . . . 7 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))
46		eleq1 2848	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑦 → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)))
47	45, 46	syl5ibrcom 250	. . . . . 6 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})) → (𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
48	47	rexlimdva 3163	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})𝑥 = ∩ 𝑦 → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
49	3, 48	biimtrid 245	. . . 4 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴)))
50		simpr 490	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ∈ V)
51		elrest 17603	. . . . . 6 ⊢ (((fi‘𝐽) ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
52	23, 50, 51	sylancr 599	. . . . 5 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴)))
53		elfi2 9409	. . . . . . . 8 ⊢ (𝐽 ∈ V → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
54	53	adantr 486	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
55		eldifsni 4749	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
56	55	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ≠ ∅)
57		iinin1 5038	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
58	56, 57	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴))
59	38	ineq1i 4113	. . . . . . . . . . . 12 ⊢ (∩ 𝑦 ∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)
60	58, 59	eqtr4di 2813	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
61		ovexd 7455	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝐽 ↾t 𝐴) ∈ V)
62		eldifi 4067	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
63	62	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ (𝒫 𝐽 ∩ Fin))
64		elfpw 9346	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin))
65	64	simplbi 502	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ⊆ 𝐽)
66	63, 65	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
67		elrestr 17604	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
68	67	3expa 1136	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
69	68	ralrimiva 3154	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
70	69	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
71		ssralv 3977	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝐽 → (∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)))
72	66, 70, 71	sylc 66	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
73	63	elin2d 4102	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → 𝑦 ∈ Fin)
74		iinfi 9412	. . . . . . . . . . . 12 ⊢ (((𝐽 ↾t 𝐴) ∈ V ∧ (∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
75	61, 72, 56, 73, 74	syl13anc 1399	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
76	60, 75	eqeltrrd 2861	. . . . . . . . . 10 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))
77		eleq1 2848	. . . . . . . . . 10 ⊢ (𝑥 = (∩ 𝑦 ∩ 𝐴) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))))
78	76, 77	syl5ibrcom 250	. . . . . . . . 9 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))
79		ineq1 4110	. . . . . . . . . . 11 ⊢ (𝑧 = ∩ 𝑦 → (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴))
80	79	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) ↔ 𝑥 = (∩ 𝑦 ∩ 𝐴)))
81	80	imbi1d 344	. . . . . . . . 9 ⊢ (𝑧 = ∩ 𝑦 → ((𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))) ↔ (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
82	78, 81	syl5ibrcom 250	. . . . . . . 8 ⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})) → (𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
83	82	rexlimdva 3163	. . . . . . 7 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦 → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
84	54, 83	sylbid 243	. . . . . 6 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))))
85	84	rexlimdv 3161	. . . . 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 2758	. 2 ⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴))
89		fi0 9415	. . 3 ⊢ (fi‘∅) = ∅
90		relxp 5668	. . . . . 6 ⊢ Rel (V × V)
91		restfn 17600	. . . . . . . 8 ⊢ ↾t Fn (V × V)
92	91	fndmi 6643	. . . . . . 7 ⊢ dom ↾t = (V × V)
93	92	releqi 5753	. . . . . 6 ⊢ (Rel dom ↾t ↔ Rel (V × V))
94	90, 93	mpbir 234	. . . . 5 ⊢ Rel dom ↾t
95	94	ovprc 7458	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ∅)
96	95	fveq2d 6889	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = (fi‘∅))
97		ianor 997	. . . 4 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) ↔ (¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V))
98		fvprc 6877	. . . . . . 7 ⊢ (¬ 𝐽 ∈ V → (fi‘𝐽) = ∅)
99	98	oveq1d 7435	. . . . . 6 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = (∅ ↾t 𝐴))
100		0rest 17605	. . . . . 6 ⊢ (∅ ↾t 𝐴) = ∅
101	99, 100	eqtrdi 2811	. . . . 5 ⊢ (¬ 𝐽 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
102	94	ovprc2 7460	. . . . 5 ⊢ (¬ 𝐴 ∈ V → ((fi‘𝐽) ↾t 𝐴) = ∅)
103	101, 102	jaoi 871	. . . 4 ⊢ ((¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V) → ((fi‘𝐽) ↾t 𝐴) = ∅)
104	97, 103	sylbi 220	. . 3 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → ((fi‘𝐽) ↾t 𝐴) = ∅)
105	89, 96, 104	3eqtr4a 2821	. 2 ⊢ (¬ (𝐽 ∈ V ∧ 𝐴 ∈ V) → (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴))
106	88, 105	pm2.61i 184	1 ⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045   ∩ cin 4089  ∅c0 4278  𝒫 cpw 4556  {csn 4584  ∩ cint 4906  ∩ ciin 4951   × cxp 5648  dom cdm 5650  ran crn 5651  Rel wrel 5655   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420  Fincfn 8976  ficfi 9405   ↾_t crest 17596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-1o 8479  df-en 8977  df-dom 8978  df-fin 8980  df-fi 9406  df-rest 17598

This theorem is used by:  ordtrest2  23527  xkoptsub  23978  ordtrest2NEW  34601  ptrest  38630