Theorem rcfpfillem6 10568

Description: Lemma for rcfpfil 10569.

Assertion

Ref	Expression
rcfpfillem6	⊢ ((u ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))} ⋀ v ⊆ A ⋀ u ⊆ v) → v ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))})

Distinct variable group:   A,b,u,v,x

Proof of Theorem rcfpfillem6

Step	Hyp	Ref	Expression
1		visset 1816	. . . . 5 ⊢ u ∈ V
2		rcfpfillem1 10563	. . . . . 6 ⊢ (u ∈ V → (u ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))} ↔ ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ u = (A ∖ b))))
3		sseq1 2085	. . . . . . . 8 ⊢ (b = c → (b ⊆ A ↔ c ⊆ A))
4		eleq1 1537	. . . . . . . 8 ⊢ (b = c → (b ∈ Fin ↔ c ∈ Fin))
5		difeq2 2157	. . . . . . . . 9 ⊢ (b = c → (A ∖ b) = (A ∖ c))
6	5	eqeq2d 1489	. . . . . . . 8 ⊢ (b = c → (u = (A ∖ b) ↔ u = (A ∖ c)))
7	3, 4, 6	3anbi123d 895	. . . . . . 7 ⊢ (b = c → ((b ⊆ A ⋀ b ∈ Fin ⋀ u = (A ∖ b)) ↔ (c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c))))
8	7	cbvexv 1317	. . . . . 6 ⊢ (∃b(b ⊆ A ⋀ b ∈ Fin ⋀ u = (A ∖ b)) ↔ ∃c(c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)))
9	2, 8	syl6bb 538	. . . . 5 ⊢ (u ∈ V → (u ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))} ↔ ∃c(c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c))))
10	1, 9	ax-mp 7	. . . 4 ⊢ (u ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))} ↔ ∃c(c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)))
11		visset 1816	. . . . . . . . 9 ⊢ c ∈ V
12		difexg 2727	. . . . . . . . 9 ⊢ (c ∈ V → (c ∖ (v ∖ u)) ∈ V)
13	11, 12	ax-mp 7	. . . . . . . 8 ⊢ (c ∖ (v ∖ u)) ∈ V
14		sseq1 2085	. . . . . . . . 9 ⊢ (b = (c ∖ (v ∖ u)) → (b ⊆ A ↔ (c ∖ (v ∖ u)) ⊆ A))
15		eleq1 1537	. . . . . . . . 9 ⊢ (b = (c ∖ (v ∖ u)) → (b ∈ Fin ↔ (c ∖ (v ∖ u)) ∈ Fin))
16		difeq2 2157	. . . . . . . . . 10 ⊢ (b = (c ∖ (v ∖ u)) → (A ∖ b) = (A ∖ (c ∖ (v ∖ u))))
17	16	eqeq2d 1489	. . . . . . . . 9 ⊢ (b = (c ∖ (v ∖ u)) → (v = (A ∖ b) ↔ v = (A ∖ (c ∖ (v ∖ u)))))
18	14, 15, 17	3anbi123d 895	. . . . . . . 8 ⊢ (b = (c ∖ (v ∖ u)) → ((b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b)) ↔ ((c ∖ (v ∖ u)) ⊆ A ⋀ (c ∖ (v ∖ u)) ∈ Fin ⋀ v = (A ∖ (c ∖ (v ∖ u))))))
19	13, 18	cla4ev 1872	. . . . . . 7 ⊢ (((c ∖ (v ∖ u)) ⊆ A ⋀ (c ∖ (v ∖ u)) ∈ Fin ⋀ v = (A ∖ (c ∖ (v ∖ u)))) → ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b)))
20		ssdifss 2171	. . . . . . . . 9 ⊢ (c ⊆ A → (c ∖ (v ∖ u)) ⊆ A)
21	20	3ad2ant1 802	. . . . . . . 8 ⊢ ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (c ∖ (v ∖ u)) ⊆ A)
22	21	3ad2ant1 802	. . . . . . 7 ⊢ (((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) ⋀ v ⊆ A ⋀ u ⊆ v) → (c ∖ (v ∖ u)) ⊆ A)
23		difss 2170	. . . . . . . . . 10 ⊢ (c ∖ (v ∖ u)) ⊆ c
24		ssfi 4547	. . . . . . . . . 10 ⊢ ((c ∈ Fin ⋀ (c ∖ (v ∖ u)) ⊆ c) → (c ∖ (v ∖ u)) ∈ Fin)
25	23, 24	mpan2 698	. . . . . . . . 9 ⊢ (c ∈ Fin → (c ∖ (v ∖ u)) ∈ Fin)
26	25	3ad2ant2 803	. . . . . . . 8 ⊢ ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (c ∖ (v ∖ u)) ∈ Fin)
27	26	3ad2ant1 802	. . . . . . 7 ⊢ (((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) ⋀ v ⊆ A ⋀ u ⊆ v) → (c ∖ (v ∖ u)) ∈ Fin)
28		dfss4 2245	. . . . . . . . . . . . . . . . . . 19 ⊢ (c ⊆ A ↔ (A ∖ (A ∖ c)) = c)
29		difeq2 2157	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (u = (A ∖ c) → (A ∖ u) = (A ∖ (A ∖ c)))
30	29	eqcomd 1483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (u = (A ∖ c) → (A ∖ (A ∖ c)) = (A ∖ u))
31	30	eqeq1d 1486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (u = (A ∖ c) → ((A ∖ (A ∖ c)) = c ↔ (A ∖ u) = c))
32	31	biimpd 153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = (A ∖ c) → ((A ∖ (A ∖ c)) = c → (A ∖ u) = c))
33		undif 2347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (u ⊆ v ↔ (u ∪ (v ∖ u)) = v)
34		difeq2 2157	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((u ∪ (v ∖ u)) = v → (A ∖ (u ∪ (v ∖ u))) = (A ∖ v))
35	33, 34	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (u ⊆ v → (A ∖ (u ∪ (v ∖ u))) = (A ∖ v))
36		difun1 2266	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (A ∖ (u ∪ (v ∖ u))) = ((A ∖ u) ∖ (v ∖ u))
37	35, 36	syl5eqr 1524	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (u ⊆ v → ((A ∖ u) ∖ (v ∖ u)) = (A ∖ v))
38	37	eqeq1d 1486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (u ⊆ v → (((A ∖ u) ∖ (v ∖ u)) = (c ∖ (v ∖ u)) ↔ (A ∖ v) = (c ∖ (v ∖ u))))
39		difeq1 2156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((A ∖ u) = c → ((A ∖ u) ∖ (v ∖ u)) = (c ∖ (v ∖ u)))
40	38, 39	syl5cbi 209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A ∖ u) = c → (u ⊆ v → (A ∖ v) = (c ∖ (v ∖ u))))
41	32, 40	syl6com 53	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((A ∖ (A ∖ c)) = c → (u = (A ∖ c) → (u ⊆ v → (A ∖ v) = (c ∖ (v ∖ u)))))
42	41	a1d 12	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ∖ (A ∖ c)) = c → (c ∈ Fin → (u = (A ∖ c) → (u ⊆ v → (A ∖ v) = (c ∖ (v ∖ u))))))
43	28, 42	sylbi 199	. . . . . . . . . . . . . . . . . 18 ⊢ (c ⊆ A → (c ∈ Fin → (u = (A ∖ c) → (u ⊆ v → (A ∖ v) = (c ∖ (v ∖ u))))))
44	43	3imp 829	. . . . . . . . . . . . . . . . 17 ⊢ ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (u ⊆ v → (A ∖ v) = (c ∖ (v ∖ u))))
45	44	impcom 351	. . . . . . . . . . . . . . . 16 ⊢ ((u ⊆ v ⋀ (c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c))) → (A ∖ v) = (c ∖ (v ∖ u)))
46	45	difeq2d 2162	. . . . . . . . . . . . . . 15 ⊢ ((u ⊆ v ⋀ (c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c))) → (A ∖ (A ∖ v)) = (A ∖ (c ∖ (v ∖ u))))
47	46	eqeq2d 1489	. . . . . . . . . . . . . 14 ⊢ ((u ⊆ v ⋀ (c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c))) → (v = (A ∖ (A ∖ v)) ↔ v = (A ∖ (c ∖ (v ∖ u)))))
48	47	biimpd 153	. . . . . . . . . . . . 13 ⊢ ((u ⊆ v ⋀ (c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c))) → (v = (A ∖ (A ∖ v)) → v = (A ∖ (c ∖ (v ∖ u)))))
49	48	ex 373	. . . . . . . . . . . 12 ⊢ (u ⊆ v → ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (v = (A ∖ (A ∖ v)) → v = (A ∖ (c ∖ (v ∖ u))))))
50	49	com13 33	. . . . . . . . . . 11 ⊢ (v = (A ∖ (A ∖ v)) → ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (u ⊆ v → v = (A ∖ (c ∖ (v ∖ u))))))
51	50	eqcoms 1481	. . . . . . . . . 10 ⊢ ((A ∖ (A ∖ v)) = v → ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (u ⊆ v → v = (A ∖ (c ∖ (v ∖ u))))))
52	51	com12 11	. . . . . . . . 9 ⊢ ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → ((A ∖ (A ∖ v)) = v → (u ⊆ v → v = (A ∖ (c ∖ (v ∖ u))))))
53		dfss4 2245	. . . . . . . . 9 ⊢ (v ⊆ A ↔ (A ∖ (A ∖ v)) = v)
54	52, 53	syl5ib 206	. . . . . . . 8 ⊢ ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (v ⊆ A → (u ⊆ v → v = (A ∖ (c ∖ (v ∖ u))))))
55	54	3imp 829	. . . . . . 7 ⊢ (((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) ⋀ v ⊆ A ⋀ u ⊆ v) → v = (A ∖ (c ∖ (v ∖ u))))
56	19, 22, 27, 55	syl3anc 860	. . . . . 6 ⊢ (((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) ⋀ v ⊆ A ⋀ u ⊆ v) → ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b)))
57	56	3exp 834	. . . . 5 ⊢ ((c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (v ⊆ A → (u ⊆ v → ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b)))))
58	57	19.23aiv 1297	. . . 4 ⊢ (∃c(c ⊆ A ⋀ c ∈ Fin ⋀ u = (A ∖ c)) → (v ⊆ A → (u ⊆ v → ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b)))))
59	10, 58	sylbi 199	. . 3 ⊢ (u ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))} → (v ⊆ A → (u ⊆ v → ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b)))))
60	59	3imp 829	. 2 ⊢ ((u ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))} ⋀ v ⊆ A ⋀ u ⊆ v) → ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b)))
61		visset 1816	. . 3 ⊢ v ∈ V
62		eqeq1 1484	. . . . 5 ⊢ (x = v → (x = (A ∖ b) ↔ v = (A ∖ b)))
63	62	3anbi3d 901	. . . 4 ⊢ (x = v → ((b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b)) ↔ (b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b))))
64	63	exbidv 1281	. . 3 ⊢ (x = v → (∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b)) ↔ ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b))))
65	61, 64	elab 1900	. 2 ⊢ (v ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))} ↔ ∃b(b ⊆ A ⋀ b ∈ Fin ⋀ v = (A ∖ b)))
66	60, 65	sylibr 200	1 ⊢ ((u ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))} ⋀ v ⊆ A ⋀ u ⊆ v) → v ∈ {x∣∃b(b ⊆ A ⋀ b ∈ Fin ⋀ x = (A ∖ b))})

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 777   = wceq 958   ∈ wcel 960  ∃wex 982  {cab 1466  Vcvv 1814   ∖ cdif 2047   ∪ cun 2048   ⊆ wss 2050  Fincfn 4373

This theorem is referenced by:  rcfpfil 10569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203  df-er 4267  df-en 4374  df-fin 4377

Copyright terms: Public domain