Theorem fin2so 37720

Description: Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.)

Assertion

Ref	Expression
fin2so	⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ Fin)

Proof of Theorem fin2so

Dummy variables 𝑣 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplll 774	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII)
2		ssrab2 4029	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥
3		sstr 3939	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)
4	2, 3	mpan 690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ⊆ 𝐴 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)
5		elpw2g 5275	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ FinII → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴))
6	5	biimpar 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ FinII ∧ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
7	4, 6	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
8	7	ralrimivw 3129	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9		vex 3441	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ∈ V
10	9	rabex 5281	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V
11	10	rgenw 3052	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V
12		eqid 2733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
13		eleq1 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴))
14	12, 13	ralrnmptw 7036	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴))
15	11, 14	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
16	8, 15	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17		dfss3 3919	. . . . . . . . . . . . . . 15 ⊢ (ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
18	16, 17	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
19	18	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
21	10, 12	dmmpti 6633	. . . . . . . . . . . . . . 15 ⊢ dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = 𝑥
22	21	neeq1i 2993	. . . . . . . . . . . . . 14 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23		dm0rn0 5870	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅)
24	23	necon3bii 2981	. . . . . . . . . . . . . 14 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
25	22, 24	sylbb1 237	. . . . . . . . . . . . 13 ⊢ (𝑥 ≠ ∅ → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
26	25	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
27		soss 5549	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝐴 → (𝑅 Or 𝐴 → 𝑅 Or 𝑥))
28	27	impcom 407	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → 𝑅 Or 𝑥)
29		porpss 7669	. . . . . . . . . . . . . . . . 17 ⊢ [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
30	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Or 𝑥 → [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
31		solin 5556	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣))
32		fin2solem 37719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
33		breq2 5099	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑦 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑦))
34	33	rabbidv 3403	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
36		fin2solem 37719	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥)) → (𝑦𝑅𝑣 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
37	36	ancom2s 650	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑦𝑅𝑣 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
38	32, 35, 37	3orim123d 1446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → ((𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣) → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
39	31, 38	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
40	39	ralrimivva 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 Or 𝑥 → ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
41		breq1 5098	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
42		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
43		breq2 5099	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
44	41, 42, 43	3orbi123d 1437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ((𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
45	44	ralbidv 3156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
46	12, 45	ralrnmptw 7036	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
47	11, 46	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
48	40, 47	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
49	48	r19.21bi 3225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
50	9	rabex 5281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V
51	50	rgenw 3052	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑦 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V
52	34	cbvmptv 5199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑦 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
53		breq2 5099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 [⊊] 𝑧 ↔ 𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
54		eqeq2 2745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 = 𝑧 ↔ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
55		breq1 5098	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
56	53, 54, 55	3orbi123d 1437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)))
57	52, 56	ralrnmptw 7036	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑦 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)))
58	51, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
59	49, 58	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
60	59	r19.21bi 3225	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
61	60	anasss 466	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
62	30, 61	issod 5564	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Or 𝑥 → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
63	28, 62	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
64	63	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
65	64	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
66		fin2i2 10220	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ FinII ∧ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ∧ [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
67	1, 20, 26, 65, 66	syl22anc 838	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
68	52, 50	elrnmpti 5908	. . . . . . . . . . 11 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
69	67, 68	sylib 218	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
70		ssel2 3925	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
71		sonr 5553	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Or 𝐴 ∧ 𝑧 ∈ 𝐴) → ¬ 𝑧𝑅𝑧)
72	70, 71	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥)) → ¬ 𝑧𝑅𝑧)
73	72	anassrs 467	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑧𝑅𝑧)
74	73	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑧𝑅𝑧)
75	74	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧)
76		breq1 5098	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑦 ↔ 𝑧𝑅𝑦))
77	76	elrab 3643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑦))
78	77	simplbi2 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑥 → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
80		vex 3441	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
81	80	elint2 4906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦)
82		eleq2 2822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
83	12, 82	ralrnmptw 7036	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
84	11, 83	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
85	81, 84	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
86		breq2 5099	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑧 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑧))
87	86	rabbidv 3403	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})
88	87	eleq2d 2819	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑧 → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
89	88	rspcv 3569	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
90		breq1 5098	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑧 ↔ 𝑧𝑅𝑧))
91	90	elrab 3643	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑧))
92	91	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧} → 𝑧𝑅𝑧)
93	89, 92	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧𝑅𝑧))
94	93	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧𝑅𝑧))
95	85, 94	biimtrid 242	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) → 𝑧𝑅𝑧))
96		eleq2 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
97	96	imbi1d 341	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
98	95, 97	syl5ibcom 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
99	98	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧))
100	79, 99	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧𝑅𝑧))
101	100	adantlll 718	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧𝑅𝑧))
102	75, 101	mtod 198	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦)
103	102	ex 412	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦))
104	103	ralrimdva 3133	. . . . . . . . . . . . 13 ⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
105	104	reximdva 3146	. . . . . . . . . . . 12 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
106	105	adantll 714	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
107	106	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
108	69, 107	mpd 15	. . . . . . . . 9 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
109	108	expl 457	. . . . . . . 8 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
110	109	alrimiv 1928	. . . . . . 7 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
111		df-fr 5574	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
112	110, 111	sylibr 234	. . . . . 6 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113		simpr 484	. . . . . 6 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114		df-we 5576	. . . . . 6 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
115	112, 113, 114	sylanbrc 583	. . . . 5 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 We 𝐴)
116		weinxp 5706	. . . . 5 ⊢ (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117	115, 116	sylib 218	. . . 4 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118		sqxpexg 7697	. . . . . 6 ⊢ (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119		incom 4158	. . . . . . 7 ⊢ (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120		inex1g 5261	. . . . . . 7 ⊢ ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121	119, 120	eqeltrid 2837	. . . . . 6 ⊢ ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122		weeq1 5608	. . . . . . 7 ⊢ (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123	122	spcegv 3548	. . . . . 6 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
124	118, 121, 123	3syl 18	. . . . 5 ⊢ (𝐴 ∈ FinII → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
125	124	imp 406	. . . 4 ⊢ ((𝐴 ∈ FinII ∧ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴)
126	117, 125	syldan 591	. . 3 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴)
127		ween 9937	. . 3 ⊢ (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128	126, 127	sylibr 234	. 2 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129		fin23 10291	. . . . 5 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinIII)
130		fin34 10292	. . . . 5 ⊢ (𝐴 ∈ FinIII → 𝐴 ∈ FinIV)
131		fin45 10294	. . . . 5 ⊢ (𝐴 ∈ FinIV → 𝐴 ∈ FinV)
132	129, 130, 131	3syl 18	. . . 4 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinV)
133		fin56 10295	. . . 4 ⊢ (𝐴 ∈ FinV → 𝐴 ∈ FinVI)
134		fin67 10297	. . . 4 ⊢ (𝐴 ∈ FinVI → 𝐴 ∈ FinVII)
135	132, 133, 134	3syl 18	. . 3 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinVII)
136		fin71num 10299	. . . 4 ⊢ (𝐴 ∈ dom card → (𝐴 ∈ FinVII ↔ 𝐴 ∈ Fin))
137	136	biimpac 478	. . 3 ⊢ ((𝐴 ∈ FinVII ∧ 𝐴 ∈ dom card) → 𝐴 ∈ Fin)
138	135, 137	sylan 580	. 2 ⊢ ((𝐴 ∈ FinII ∧ 𝐴 ∈ dom card) → 𝐴 ∈ Fin)
139	128, 138	syldan 591	1 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1085  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2929  ∀wral 3048  ∃wrex 3057  {crab 3396  Vcvv 3437   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  𝒫 cpw 4551  ∩ cint 4899   class class class wbr 5095   ↦ cmpt 5176   Po wpo 5527   Or wor 5528   Fr wfr 5571   We wwe 5573   × cxp 5619  dom cdm 5621  ran crn 5622   [⊊] crpss 7664  Fincfn 8879  cardccrd 9839  Fin^IIcfin2 10181  Fin^IVcfin4 10182  Fin^IIIcfin3 10183  Fin^Vcfin5 10184  Fin^VIcfin6 10185  Fin^VIIcfin7 10186

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 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-inf2 9542

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-rmo 3347  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 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-isom 6498  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-rpss 7665  df-om 7806  df-1st 7930  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-seqom 8376  df-1o 8394  df-2o 8395  df-er 8631  df-map 8761  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-oi 9407  df-wdom 9462  df-dju 9805  df-card 9843  df-fin2 10188  df-fin4 10189  df-fin3 10190  df-fin5 10191  df-fin6 10192  df-fin7 10193

This theorem is referenced by: (None)