tz7.49 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tz7.49		Structured version Visualization version GIF version

Theorem tz7.49 8483

Description: Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 10-Jan-2013.)

**Hypotheses**
Ref	Expression
tz7.49.1	⊢ 𝐹 Fn On
tz7.49.2	⊢ (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))

**Assertion**
Ref	Expression
tz7.49	⊢ ((𝐴 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥)))

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐹,𝑦 𝜑,𝑦 Allowed substitution hints: 𝜑(𝑥) 𝐵(𝑥,𝑦)

Proof of Theorem tz7.49 Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ne 2938	. . . . . . . . 9 ⊢ ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅)
2	1	ralbii 3090	. . . . . . . 8 ⊢ (∀𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ ↔ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅)
3		tz7.49.2	. . . . . . . . 9 ⊢ (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))
4		ralim 3083	. . . . . . . . 9 ⊢ (∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → (∀𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))
5	3, 4	sylbi 217	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))
6	2, 5	biimtrrid 243	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))
7		tz7.49.1	. . . . . . . . 9 ⊢ 𝐹 Fn On
8	7	tz7.48-3 8482	. . . . . . . 8 ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ 𝐴 ∈ V)
9		elex 3498	. . . . . . . 8 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
10	8, 9	nsyl3 138	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ¬ ∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))
11	6, 10	nsyli 157	. . . . . 6 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅))
12		dfrex2 3070	. . . . . 6 ⊢ (∃𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ↔ ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅)
13	11, 12	imbitrrdi 252	. . . . 5 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) = ∅))
14		imaeq2 6075	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦))
15	14	difeq2d 4135	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐴 ∖ (𝐹 “ 𝑥)) = (𝐴 ∖ (𝐹 “ 𝑦)))
16	15	eqeq1d 2736	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ↔ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅))
17	16	onminex 7821	. . . . 5 ⊢ (∃𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅))
18	13, 17	syl6 35	. . . 4 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅)))
19		df-ne 2938	. . . . . . 7 ⊢ ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅)
20	19	ralbii 3090	. . . . . 6 ⊢ (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ↔ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅)
21	20	anbi2i 623	. . . . 5 ⊢ (((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ↔ ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅))
22	21	rexbii 3091	. . . 4 ⊢ (∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ↔ ∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅))
23	18, 22	imbitrrdi 252	. . 3 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅)))
24		nfra1 3281	. . . . 5 ⊢ Ⅎ𝑥∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))
25	3, 24	nfxfr 1849	. . . 4 ⊢ Ⅎ𝑥𝜑
26		simpllr 776	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅)
27		fnfun 6668	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn On → Fun 𝐹)
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ Fun 𝐹
29		fvelima 6973	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ (𝐹 “ 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑧)
30	28, 29	mpan 690	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝐹 “ 𝑥) → ∃𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑧)
31		nfv 1911	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝜑
32		nfra1 3281	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅
33	31, 32	nfan 1896	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦(𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅)
34		nfv 1911	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦(𝑥 ∈ On → 𝑧 ∈ 𝐴)
35		rsp 3244	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝑦 ∈ 𝑥 → (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅))
36	35	adantld 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅))
37		onelon 6410	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
38	15	neeq1d 2997	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ ↔ (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅))
39		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
40	39, 15	eleq12d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) ↔ (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦))))
41	38, 40	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑦 → (((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) ↔ ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
42	41	rspcv 3617	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On → (∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
43	3, 42	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (𝜑 → ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
44	43	com23 86	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ On → ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝜑 → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
45	37, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝜑 → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
46	36, 45	sylcom 30	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝜑 → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
47	46	com3r 87	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
48	47	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦))))
49	48	expcomd 416	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑦 ∈ 𝑥 → (𝑥 ∈ On → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
50		eldifi 4140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)) → (𝐹‘𝑦) ∈ 𝐴)
51		eleq1 2826	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) = 𝑧 → ((𝐹‘𝑦) ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
52	50, 51	syl5ibcom 245	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)) → ((𝐹‘𝑦) = 𝑧 → 𝑧 ∈ 𝐴))
53	49, 52	syl8 76	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑦 ∈ 𝑥 → (𝑥 ∈ On → ((𝐹‘𝑦) = 𝑧 → 𝑧 ∈ 𝐴))))
54	53	com34 91	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑦 ∈ 𝑥 → ((𝐹‘𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧 ∈ 𝐴))))
55	33, 34, 54	rexlimd 3263	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (∃𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧 ∈ 𝐴)))
56	30, 55	syl5 34	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑧 ∈ (𝐹 “ 𝑥) → (𝑥 ∈ On → 𝑧 ∈ 𝐴)))
57	56	com23 86	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑥 ∈ On → (𝑧 ∈ (𝐹 “ 𝑥) → 𝑧 ∈ 𝐴)))
58	57	imp 406	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝑧 ∈ (𝐹 “ 𝑥) → 𝑧 ∈ 𝐴))
59	58	ssrdv 4000	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝐹 “ 𝑥) ⊆ 𝐴)
60		ssdif0 4371	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ (𝐹 “ 𝑥) ↔ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅)
61	60	biimpri 228	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → 𝐴 ⊆ (𝐹 “ 𝑥))
62	59, 61	anim12i 613	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → ((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐹 “ 𝑥)))
63		eqss 4010	. . . . . . . . . 10 ⊢ ((𝐹 “ 𝑥) = 𝐴 ↔ ((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐹 “ 𝑥)))
64	62, 63	sylibr 234	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → (𝐹 “ 𝑥) = 𝐴)
65		onss 7803	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
66	32, 31	nfan 1896	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑)
67		nfv 1911	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦 𝑥 ⊆ On
68	66, 67	nfan 1896	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On)
69		nfv 1911	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑧(((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦 ∈ 𝑥)
70		ssel 3988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → 𝑦 ∈ On))
71		onss 7803	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
72	7	fndmi 6672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom 𝐹 = On
73	71, 72	sseqtrrdi 4046	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ On → 𝑦 ⊆ dom 𝐹)
74		funfvima2 7250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun 𝐹 ∧ 𝑦 ⊆ dom 𝐹) → (𝑧 ∈ 𝑦 → (𝐹‘𝑧) ∈ (𝐹 “ 𝑦)))
75	28, 73, 74	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ On → (𝑧 ∈ 𝑦 → (𝐹‘𝑧) ∈ (𝐹 “ 𝑦)))
76	70, 75	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑦 → (𝐹‘𝑧) ∈ (𝐹 “ 𝑦))))
77	35	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅))
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅)))
79	70, 78, 44	syl10 79	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝜑 → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦))))))
80	79	imp4a 422	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
81		eldifn 4141	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)) → ¬ (𝐹‘𝑦) ∈ (𝐹 “ 𝑦))
82		eleq1a 2833	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → ((𝐹‘𝑦) = (𝐹‘𝑧) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑦)))
83	82	con3d 152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → (¬ (𝐹‘𝑦) ∈ (𝐹 “ 𝑦) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
84	81, 83	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)) → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
85	80, 84	syl8 76	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))))
86	85	com34 91	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))))
87	76, 86	syldd 72	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑦 → ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))))
88	87	com4r 94	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))))
89	88	imp31 417	. . . . . . . . . . . . . . . . . 18 ⊢ ((((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦 ∈ 𝑥) → (𝑧 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
90	69, 89	ralrimi 3254	. . . . . . . . . . . . . . . . 17 ⊢ ((((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦 ∈ 𝑥) → ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧))
91	90	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → (𝑦 ∈ 𝑥 → ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
92	68, 91	ralrimi 3254	. . . . . . . . . . . . . . 15 ⊢ (((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧))
93	92	ex 412	. . . . . . . . . . . . . 14 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
94	93	ancld 550	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧))))
95	7	tz7.48lem 8479	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧)) → Fun ^◡(𝐹 ↾ 𝑥))
96	65, 94, 95	syl56 36	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ∈ On → Fun ^◡(𝐹 ↾ 𝑥)))
97	96	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑥 ∈ On → Fun ^◡(𝐹 ↾ 𝑥)))
98	97	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → Fun ^◡(𝐹 ↾ 𝑥))
99	98	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → Fun ^◡(𝐹 ↾ 𝑥))
100	26, 64, 99	3jca 1127	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥)))
101	100	exp41 434	. . . . . . 7 ⊢ (𝜑 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝑥 ∈ On → ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))))
102	101	com23 86	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))))
103	102	com34 91	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ On → ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))))
104	103	imp4a 422	. . . 4 ⊢ (𝜑 → (𝑥 ∈ On → (((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥)))))
105	25, 104	reximdai 3258	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))
106	23, 105	syld 47	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))
107	106	impcom 407	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1536 ∈ wcel 2105 ≠ wne 2937 ∀wral 3058 ∃wrex 3067 Vcvv 3477 ∖ cdif 3959 ⊆ wss 3962 ∅c0 4338 ^◡ccnv 5687 dom cdm 5688 ↾ cres 5690 “ cima 5691 Oncon0 6385 Fun wfun 6556 Fn wfn 6557 ‘cfv 6562

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pr 5437 ax-un 7753

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-ral 3059 df-rex 3068 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-int 4951 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-ord 6388 df-on 6389 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570

This theorem is referenced by: tz7.49c 8484

W3C validator